period_le_of_fixed — Mathlib

English

If Hk is IsMultiplyPretransitive G α k and s ⊆ α with card k, then (fixingSubgroup G s).index = choose(|α|, k) · k!.

Русский

Если Hk = IsMultiplyPretransitive G α k и s ⊆ α с кардинальностью k, то индекс fixingSubgroup G s равен C(|α|, k) · k!.

LaTeX

$$(fixingSubgroup G s).index = \binom{|α|}{|s|} \; |s|!$$

Lean4

/-- If for some `n`, `m ^ n • a = a`, then `period m a ≤ n`. -/
@[to_additive /-- If for some `n`, `(n • m) +ᵥ a = a`, then `period m a ≤ n`. -/
    ]
theorem period_le_of_fixed {m : M} {a : α} {n : ℕ} (n_pos : 0 < n) (fixed : m ^ n • a = a) : period m a ≤ n :=
  (isPeriodicPt_smul_iff.mpr fixed).minimalPeriod_le n_pos

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