coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities

From: Daniel Schepler <dschepler AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities
Date: Thu, 14 Apr 2016 17:47:03 -0700
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=dschepler AT gmail.com; spf=Pass smtp.mailfrom=dschepler AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi0-f44.google.com
Ironport-phdr: 9a23:rO5Z2hVAIEwOh4DI8bynCJtb1FXV8LGtZVwlr6E/grcLSJyIuqrYZhOGt8tkgFKBZ4jH8fUM07OQ6PCwHzFfqsrb+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpq82VPloD2GD1SIgxBSv1hD2ZjtMRj4pmJ/R54TryiVwMRd5rw3h1L0mYhRf265T41pdi9yNNp6BprJYYAu3SNp41Rr1ADTkgL3t9pIiy7UGCHkOz4S43VXxeuR5VCUCR5xbjG5z1ryHSt+xn2SDcM9egHp4uXjH3w65tSRLswBwMNzMh9GzNwph8l6lbrQqlqgZXzIvdYYXTP/17KPCONegGTHZMC54CHxdKBZmxOs5WV7IM

On Thu, Apr 14, 2016 at 5:17 PM, Abhishek Anand
<abhishek.anand.iitg AT gmail.com>
wrote:
> Context {R:Type}`{Rid:Integral_domain R}.

I thought many boolean rings of interest were not integral domains.
For example, in a classical universe, the boolean ring corresponding
to the boolean algebra P(X) is an integral domain only if X is empty
or a singleton.
--
Daniel

[Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Abhishek Anand, 04/13/2016
- Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Laurent Thery, 04/13/2016
  - Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Laurent Thery, 04/13/2016
    - Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Abhishek Anand, 04/15/2016
      - Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Daniel Schepler, 04/15/2016
        
        Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Abhishek Anand, 04/15/2016
        
        Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Daniel Schepler, 04/15/2016
        
        Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Pierre-Marie Pédrot, 04/15/2016
      - Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Laurent Thery, 04/15/2016
        
        Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Laurent Thery, 04/15/2016
        
        Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Abhishek Anand, 04/16/2016
        
        Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Daniel Schepler, 04/16/2016
- Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Assia Mahboubi, 04/19/2016