pow_eq_pow_iff_of_coprime — Mathlib

English

For a,b in a group-with-zero, and m,n with gcd(m,n) = 1, a^m = b^n iff there exists c with a = c^n and b = c^m.

Русский

Для a,b в группе с нулем и m,n с gcd(m,n) = 1, a^m = b^n тогда и только тогда, когда существует c с a = c^n и b = c^m.

LaTeX

$$$$a^m = b^n \\iff \\exists c, a = c^n \\wedge b = c^m.$$$$

Lean4

theorem pow_eq_pow_iff_of_coprime (hmn : m.Coprime n) : a ^ m = b ^ n ↔ ∃ c, a = c ^ n ∧ b = c ^ m :=
  (Commute.all _ _).pow_eq_pow_iff_of_coprime hmn

Похожие утверждения