exponent_dvd — Mathlib

English

For a monoid G, exponent G divides n if and only if for all g in G, orderOf g divides n.

Русский

Для моноида G экспонента G делит n тогда и только тогда порядок каждого элемента делит n.

LaTeX

$$$\\\\operatorname{exponent} G \\\\mid n \\\\Longleftrightarrow \\\\forall g : G, \\\\operatorname{orderOf} g \\\\mid n$$$

Lean4

@[to_additive]
theorem exponent_dvd {n : ℕ} : exponent G ∣ n ↔ ∀ g : G, orderOf g ∣ n := by
  simp_rw [exponent_dvd_iff_forall_pow_eq_one, orderOf_dvd_iff_pow_eq_one]

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