zpow_smul_eq_iff_period_dvd — Mathlib

English

For an integer exponent j and action g on a, g^j • a = a if and only if (period g a : ℤ) divides j.

Русский

Для целочисленного показателя j и действия g на a справедливо: g^j • a = a тогда и только тогда, когда (period g a : ℤ) делит j.

LaTeX

$$$ g^j \\cdot a = a \\iff (\\operatorname{period} g a : \\mathbb{Z}) \\mid j $$$

Lean4

@[to_additive]
theorem zpow_smul_eq_iff_period_dvd {j : ℤ} {g : G} {a : α} : g ^ j • a = a ↔ (period g a : ℤ) ∣ j := by
  match j with
  | (n : ℕ) => rw [zpow_natCast, Int.natCast_dvd_natCast, pow_smul_eq_iff_period_dvd]
  | -(n + 1 : ℕ) =>
    rw [zpow_neg, zpow_natCast, inv_smul_eq_iff, eq_comm, Int.dvd_neg, Int.natCast_dvd_natCast,
      pow_smul_eq_iff_period_dvd]

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