Def Order.Frame.MinimalAxioms.Order.Coframe.MinimalAxioms.CompleteDistribLattice.MinimalAxioms.CompletelyDistribLattice.MinimalAxioms.of

Modification history

2024-07-23 12:07

Mathlib/Order/CompleteBooleanAlgebra.lean

refactor: Make `Frame` extend `HeytingAlgebra` (#10560) …

Added Order.Frame.MinimalAxioms.Order.Coframe.MinimalAxioms.CompleteDistribLattice.MinimalAxioms.CompletelyDistribLattice.MinimalAxioms.of View on Github →