exponent_dvd_iff_forall_zpow_eq_one

English

For a group G and integer n, (exponent G as integer) divides n iff every element of G raised to n is the identity.

Русский

Для группы G и целого n выражение (exponent G) делит n тогда, когда для каждого элемента g группы G выполняется g^n = 1.

LaTeX

$$$(\operatorname{exponent} G : \mathbb{Z}) \mid n \iff \forall g : G, g^n = 1$$$

Lean4

@[to_additive]
theorem exponent_dvd_iff_forall_zpow_eq_one : (Monoid.exponent G : ℤ) ∣ n ↔ ∀ g : G, g ^ n = 1 := by
  simp_rw [Int.natCast_dvd, Monoid.exponent_dvd_iff_forall_pow_eq_one, pow_natAbs_eq_one]

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