English
If x^m = 1 and x^n = 1 in a group-with-zero, then x^{gcd(m,n)} = 1.
Русский
Если x^m = 1 и x^n = 1 в группе с нулем, тогда x^{gcd(m,n)} = 1.
LaTeX
$$$$x^m = 1 \\wedge x^n = 1 \\Rightarrow x^{\\gcd(m,n)} = 1.$$$$
Lean4
protected theorem pow_eq_pow_iff_of_coprime (hab : Commute a b) (hmn : m.Coprime n) :
a ^ m = b ^ n ↔ ∃ c, a = c ^ n ∧ b = c ^ m :=
by
refine ⟨fun h ↦ ?_, by rintro ⟨c, rfl, rfl⟩; rw [← pow_mul, ← pow_mul']⟩
by_cases m = 0; · simp_all
by_cases n = 0; · simp_all
by_cases hb : b = 0; · exact ⟨0, by simp_all⟩
by_cases ha : a = 0; · exact ⟨0, by have := h.symm; simp_all⟩
refine ⟨a ^ Nat.gcdB m n * b ^ Nat.gcdA m n, ?_, ?_⟩ <;>
· refine (pow_one _).symm.trans ?_
conv_lhs => rw [← zpow_natCast, ← hmn, Nat.gcd_eq_gcd_ab]
simp only [zpow_add₀ ha, zpow_add₀ hb, ← zpow_natCast, (hab.zpow_zpow₀ _ _).mul_zpow, ← zpow_mul,
mul_comm (Nat.gcdB m n), mul_comm (Nat.gcdA m n)]
simp only [zpow_mul, zpow_natCast, h]
exact ((Commute.pow_pow (by aesop) _ _).zpow_zpow₀ _ _).symm
