mathlib
b8b18fa5 - feat(order/complete_boolean_algebra): A frame is distributive (#15340)

Commit

3 years ago

feat(order/complete_boolean_algebra): A frame is distributive (#15340) `frame α`/`coframe α` imply `distrib_lattice α`.

Author

YaelDillies

Parents