English
For a monoid G, exponent G divides n if and only if every element g satisfies g^n = 1.
Русский
Для моноида G показатель экспоненты делит n тогда и только тогда каждый элемент g удовлетворяет g^n = 1.
LaTeX
$$$\\\\operatorname{exponent} G \\\\mid n \\\\Longleftrightarrow \\\\forall g : G, \\\\operatorname{pow}(g,n) = 1$$$
Lean4
@[to_additive]
theorem exponent_dvd_iff_forall_pow_eq_one {n : ℕ} : exponent G ∣ n ↔ ∀ g : G, g ^ n = 1 :=
by
rcases n.eq_zero_or_pos with (rfl | hpos)
· simp
constructor
· intro h g
rw [Nat.dvd_iff_mod_eq_zero] at h
rw [pow_eq_mod_exponent, h, pow_zero]
· intro hG
by_contra h
rw [Nat.dvd_iff_mod_eq_zero, ← Ne, ← pos_iff_ne_zero] at h
have h₂ : n % exponent G < exponent G := Nat.mod_lt _ (exponent_pos_of_exists n hpos hG)
have h₃ : exponent G ≤ n % exponent G := by
apply exponent_min' _ h
simp_rw [← pow_eq_mod_exponent]
exact hG
exact h₂.not_ge h₃
