Theorem mul_inv_cancel

Modification history

2024-08-12 15:04
Mathlib/Algebra/Group/Defs.lean
chore: deduplicate `inv_mul_cancel`/`mul_inv_cancel`, etc. (#15717) …
Modified mul_inv_cancelView on Github →
2024-04-27 06:15
Mathlib/Algebra/GroupWithZero/Defs.lean
feat: Axiomatise `b ≠ 0 → a * b / b = a` (#12424) …
Modified mul_inv_cancelView on Github →
2022-11-26 15:48
Mathlib/Algebra/GroupWithZero/Defs.lean
chore: make argument to mul_inv_cancel implicit (#737) …
Added mul_inv_cancelView on Github →