Theorem pow_injective_of_not_unit

Modification history

2024-09-24 00:42
Mathlib/Algebra/Associated/Basic.lean
chore(UniqueFactorizationDomain): drop `pow_right_injective` (#17012) …
Deleted pow_injective_of_not_unitView on Github →
2022-12-20 05:33
Mathlib/Algebra/Associated.lean
feat: port Algebra.Associated (#1098) …
Added pow_injective_of_not_unitView on Github →