Mathlib Changelog
v4
Changelog
About
Github
Theorem
ofLex_eq_one
Modification history
2025-08-19 23:16
Mathlib/Algebra/Order/Group/Synonym.lean
chore(HahnSeries): make more usable, golf (#28632) …
Added
ofLex_eq_one
View on Github →