Commit 2024-11-18 21:32 dc324b56

View on Github →

feat: right-division as an OrderIso (#19191)

Estimated changes

Modified Mathlib/Algebra/GroupWithZero/Units/Equiv.lean

added def Equiv.divRight₀

modified theorem mulLeft_bijective₀

modified theorem mulRight_bijective₀

Modified Mathlib/Algebra/Order/GroupWithZero/Unbundled/Lemmas.lean

added def OrderIso.divRight₀