mathlib
3d369087 - fix(order/bounded_order): remove classical axiom from Prop.distrib_lattice (#16497)

Commit

3 years ago

fix(order/bounded_order): remove classical axiom from Prop.distrib_lattice (#16497) Used all three axioms before, now only `propext`.

Author

alreadydone

Parents