Theorem Group.isUnit

Modification history

2024-08-12 15:04

Mathlib/Algebra/Group/Units.lean

chore: deduplicate `inv_mul_cancel`/`mul_inv_cancel`, etc. (#15717) …

Modified Group.isUnit View on Github →

2024-01-09 09:25

Mathlib/Algebra/Group/Units.lean

feat: `a / b = c / d ↔ a * d = c * b` when `b`, `d` commute (#9389) …

Modified Group.isUnit View on Github →

2022-12-03 03:40

Mathlib/Algebra/Hom/Units.lean

feat: port Algebra.Hom.Units (#745) …

Added Group.isUnit View on Github →