support_pow_of_pos_of_lt_orderOf — Mathlib

English

If f is a cycle and 0 < n < orderOf(f), then the support of f^n equals the support of f.

Русский

Если f — цикл и 0 < n < orderOf(f), то поддержка f^n совпадает с поддержкой f.

LaTeX

$$$\\forall f:\\mathrm{Perm}(\\alpha), \\mathrm{IsCycle}(f) \\Rightarrow \\forall n\\in \\mathbb{N},\\; 0 < n \\land n < \\mathrm{orderOf}(f) \\Rightarrow \\mathrm{supp}(f^n) = \\mathrm{supp}(f).$$$

Lean4

theorem support_pow_of_pos_of_lt_orderOf (hf : IsCycle f) {n : ℕ} (npos : 0 < n) (hn : n < orderOf f) :
    (f ^ n).support = f.support :=
  hf.support_pow_eq_iff.2 <| Nat.not_dvd_of_pos_of_lt npos hn

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