Def OrderIso.divRight₀

Modification history

2025-04-11 08:18

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

feat(Order/GroupWithZero): drop more TC assumptions (#23922) …

Modified OrderIso.divRight₀ View on Github →

2025-04-10 02:58

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

feat(Order/GroupWithZero): drop some `0 ≤ 1` assumptions (#23892) …

Modified OrderIso.divRight₀ View on Github →

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 →