Commit 2024-11-17 16:59 561dec6d

View on Github →

feat: (WithZero α)ˣ is isomorphic to α as an ordered group (#18986) From FLT

Estimated changes

Modified Mathlib/Algebra/Order/GroupWithZero/Canonical.lean

added theorem WithZero.unzero_le_unzero

Modified Mathlib/Algebra/Order/Hom/Monoid.lean

added def OrderMonoidIso.unitsWithZero