Def Invertible.mul

Modification history

2024-05-07 01:05

Mathlib/Algebra/Invertible/Defs.lean

refactor: replace `@[reducible]` with `abbrev` (#12614) …

Deleted Invertible.mul View on Github →

2023-09-06 11:21

Mathlib/Algebra/Invertible.lean

chore: split Mathlib.Algebra.Invertible (#6973) …

Modified Invertible.mul View on Github →

2023-06-22 09:57

Mathlib/Algebra/Invertible.lean

chore: forward-port mathlib#19204 (#5369)

Added Invertible.mul View on Github →