mathlib3
e4fb6414 - feat(order/heyting/basic): Generalize boolean algebras lemmas (#16281)

Commit
3 years ago
feat(order/heyting/basic): Generalize boolean algebras lemmas (#16281) Generalize lemmas from `(generalized_)boolean_algebra` to `(generalized_)coheyting_algebra`. Dualize (some of) them. Duplicate lemmas have been made aliases. Add supporting lemmas to golf the proofs. Co-authored-by: Mauricio Collares <mauricio@collares.org>
Author
Parents
Loading