Def OrderIso.divRight₀

Modification history

2024-11-20 10:54

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

chore: deprecate `LinearOrderedCommGroupWithZero` lemmas (#19197) …

Modified OrderIso.divRight₀ View on Github →

2024-11-18 21:32

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

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

Added OrderIso.divRight₀ View on Github →