Def invertibleOfMulInvertible
Modification history
2024-05-07 01:05
Mathlib/Algebra/Invertible/Basic.lean
refactor: replace `@[reducible]` with `abbrev` (#12614) …
Deleted invertibleOfMulInvertibleView on Github →2023-09-06 11:21
Mathlib/Algebra/Invertible.lean
chore: split Mathlib.Algebra.Invertible (#6973) …
Modified invertibleOfMulInvertibleView on Github →