Def LatticeCon.mk'

Modification history

2026-01-09 08:53

Mathlib/Order/Lattice/Congruence.lean

chore(Order/Defs/Unbundled): deprecate `IsRefl` in favor of core's `Std.Refl` (#33755)

Modified LatticeCon.mk'View on Github →

2025-09-19 18:56

Mathlib/Order/Lattice/Congruence.lean

feat(Order/Lattice): conditions for an equivalence relation to be a lattice congruence (#26836) …

Added LatticeCon.mk'View on Github →