exponent_dvd_sub_iff_zpow_eq_zpow

English

The divisibility of the exponent by n−m is equivalent to g^n = g^m for all g in G.

Русский

Делимость экспоненты по разности n−m эквивалентна тому, что для всех g ∈ G выполняется g^n = g^m.

LaTeX

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

Lean4

@[to_additive]
theorem exponent_dvd_sub_iff_zpow_eq_zpow : (Monoid.exponent G : ℤ) ∣ n - m ↔ ∀ g : G, g ^ n = g ^ m := by
  simp_rw [Group.exponent_dvd_iff_forall_zpow_eq_one, zpow_sub, mul_inv_eq_one]

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