Def Lattice.mkDual

Modification history

2026-10-04 06:22
Mathlib/Order/Defs/Lattice.lean
feat(Translate): command for adding a translation (#43750) …
Deleted Lattice.mkDualView on Github →
2026-09-30 00:55
Mathlib/Order/Defs/Lattice.lean
chore(Order): move the definition of lattices to a new file (#44002) …
Modified Lattice.mkDualView on Github →
2026-08-19 10:57
Mathlib/Order/Lattice.lean
chore(Order/LatticeIntervals): use `to_dual` (#42364)
Added Lattice.mkDualView on Github →