Def DistribLattice.ofInfSupLe

Modification history

2024-05-07 01:05

Mathlib/Order/Lattice.lean

refactor: replace `@[reducible]` with `abbrev` (#12614) …

Deleted DistribLattice.ofInfSupLe View on Github →

2022-11-25 17:46

Mathlib/Order/Lattice.lean

feat: port Order.Lattice (#642) …

Added DistribLattice.ofInfSupLe View on Github →