Theorem Commute.exists_eq_pow_of_pow_eq_pow_of_coprime

Modification history

2024-01-08 12:05
Mathlib/Algebra/GroupWithZero/Power.lean
chore: Move `a ^ m = b ^ n ↔ ∃ c, a = c ^ n ∧ b = c ^ m` (#9505) …
Deleted Commute.exists_eq_pow_of_pow_eq_pow_of_coprimeView on Github →
2024-01-06 20:00
Mathlib/Algebra/GroupWithZero/Power.lean
feat: Criteria for `X ^ n - C a` to be irreducible for odd `n`. (#9397)
Added Commute.exists_eq_pow_of_pow_eq_pow_of_coprimeView on Github →