Def Equiv.divRight₀

Modification history

2024-12-05 08:47
Mathlib/Algebra/GroupWithZero/Units/Equiv.lean
feat: left division by a nonzero element as a `Perm` (#19458)
Modified Equiv.divRight₀View on Github →
2024-11-18 21:32
Mathlib/Algebra/GroupWithZero/Units/Equiv.lean
feat: right-division as an `OrderIso` (#19191)
Added Equiv.divRight₀View on Github →