English
If x^n = 1 with 0 < n, then the submonoid generated by x is a cyclic group of order n, with inverse of x being x^{n-1}.
Русский
Если x^n = 1 при 0 < n, то порожденный x подмоноид является циклической группой порядка n; обратный к x равен x^{n-1}.
LaTeX
$$$ 0 < n \\Rightarrow x^n = 1 \\Rightarrow \\operatorname{powers}(x) \\text{ is a group of order } n $$$
Lean4
/-- The submonoid generated by an element is a group if that element has finite order. -/
abbrev groupPowers {x : M} {n : ℕ} (hpos : 0 < n) (hx : x ^ n = 1) : Group (powers x)
where
inv x := x ^ (n - 1)
inv_mul_cancel
y :=
Subtype.ext <| by
obtain ⟨_, k, rfl⟩ := y
simp only [coe_one, coe_mul, SubmonoidClass.coe_pow]
rw [← pow_succ, Nat.sub_add_cancel hpos, ← pow_mul, mul_comm, pow_mul, hx, one_pow]
zpow z x := x ^ z.natMod n
zpow_zero' z := by simp only [Int.natMod, Int.zero_emod, Int.toNat_zero, pow_zero]
zpow_neg' m
x :=
Subtype.ext <| by
obtain ⟨_, k, rfl⟩ := x
simp only [← pow_mul, Int.natMod, SubmonoidClass.coe_pow]
rw [Int.negSucc_eq, ← Int.natCast_succ, ← Int.add_mul_emod_self_right (b := (m + 1 : ℕ))]
nth_rw 1 [← mul_one ((m + 1 : ℕ) : ℤ)]
rw [← sub_eq_neg_add, ← Int.mul_sub, ← Int.natCast_pred_of_pos hpos]; norm_cast
simp only [Int.toNat_natCast]
rw [mul_comm, pow_mul, ← pow_eq_pow_mod _ hx, mul_comm k, mul_assoc, pow_mul _ (_ % _), ← pow_eq_pow_mod _ hx,
pow_mul, pow_mul]
zpow_succ' m
x :=
Subtype.ext <| by
obtain ⟨_, k, rfl⟩ := x
simp only [← pow_mul, Int.natMod, SubmonoidClass.coe_pow, coe_mul]
norm_cast
iterate 2 rw [Int.toNat_natCast, mul_comm, pow_mul, ← pow_eq_pow_mod _ hx]
rw [← pow_mul _ m, mul_comm, pow_mul, ← pow_succ, ← pow_mul, mul_comm, pow_mul]
