Commit 2024-09-24 00:42 97987b25

View on Github →

chore(UniqueFactorizationDomain): drop pow_right_injective (#17012) Use more general lemmas instead

Estimated changes

Modified Mathlib/Algebra/Associated/Basic.lean

added theorem pow_inj_of_not_isUnit

added theorem pow_injective_of_not_isUnit

deleted theorem pow_injective_of_not_unit

Modified Mathlib/RingTheory/ChainOfDivisors.lean

Modified Mathlib/RingTheory/DedekindDomain/Ideal.lean

Modified Mathlib/RingTheory/UniqueFactorizationDomain.lean

deleted theorem UniqueFactorizationMonoid.pow_eq_pow_iff

deleted theorem UniqueFactorizationMonoid.pow_right_injective