Def Function.Injective.linearOrderedCommMonoidWithZero
Modification history
2024-05-07 01:05
Mathlib/Algebra/Order/GroupWithZero/Canonical.lean
refactor: replace `@[reducible]` with `abbrev` (#12614) …
Deleted Function.Injective.linearOrderedCommMonoidWithZeroView on Github →