Theorem eq_one_of_mul_right

Modification history

2024-10-14 13:31

Mathlib/Algebra/Group/Units/Basic.lean

chore(Algebra.Group.Units): split into `Defs` and `Basic` file (#17724) …

Modified eq_one_of_mul_right View on Github →

2023-04-12 19:26

Mathlib/Algebra/Group/Units.lean

feat: Dot notation aliases (#3303) …

Added eq_one_of_mul_right View on Github →