Theorem JordanHolderLattice.iso_refl

Modification history

2026-07-14 16:30

Mathlib/Order/JordanHolder.lean

refactor(Order/JordanHolder): remove `Iso` from `JordanHolderLattice` (#41445) …

Added JordanHolderLattice.iso_refl View on Github →