Theorem exists_associated_pow_of_associated_pow_mul

Modification history

2024-07-11 10:12
Mathlib/RingTheory/PrincipalIdealDomain.lean
feat(Mathlib.NumberTheory.FLT.Three): add various results (#14227) …
Added exists_associated_pow_of_associated_pow_mulView on Github →