Def unitsEquivNeZero

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 unitsEquivNeZeroView on Github →
2024-11-28 07:30
Mathlib/Algebra/GroupWithZero/Units/Basic.lean
chore: move unitsEquivNeZero later (#19437) …
Modified unitsEquivNeZeroView on Github →
2024-05-23 11:18
Mathlib/Algebra/GroupWithZero/Units/Basic.lean
chore: Remove order dependencies to `Data.Fin.Basic` (#13005) …
Modified unitsEquivNeZeroView on Github →
2023-01-16 17:55
Mathlib/Data/Fintype/Basic.lean
feat: port Data.Fintype.Basic (#1593)
Added unitsEquivNeZeroView on Github →