English
If x^m = 1 and x^n = 1 in a Monoid, 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
@[to_additive gcd_nsmul_eq_zero]
theorem pow_gcd_eq_one {M : Type*} [Monoid M] (x : M) {m n : ℕ} (hm : x ^ m = 1) (hn : x ^ n = 1) : x ^ m.gcd n = 1 :=
by
rcases m with (rfl | m); · simp [hn]
obtain ⟨y, rfl⟩ := IsUnit.of_pow_eq_one hm m.succ_ne_zero
rw [← Units.val_pow_eq_pow_val, ← Units.val_one (α := M), ← zpow_natCast, ← Units.ext_iff] at *
rw [Nat.gcd_eq_gcd_ab, zpow_add, zpow_mul, zpow_mul, hn, hm, one_zpow, one_zpow, one_mul]
