Theorem toLex_eq_one

Modification history

2025-10-14 04:17
Mathlib/Algebra/Order/Group/Synonym.lean
feat: group instances on `Colex α` (#30483) …
Modified toLex_eq_oneView on Github →
2025-08-26 23:57
Mathlib/Algebra/Order/Group/Synonym.lean
feat(RingTheory): decompose archimedean classes of HahnSeries (#25970) …
Added toLex_eq_oneView on Github →