mem_cycleFactorsFinset_conj' — Mathlib

English

Conjugating c by k preserves membership in the cycle factors finset: k•c ∈ (k•g).cycleFactorsFinset iff c ∈ g.cycleFactorsFinset.

Русский

При сопряжении c на k сохраняется принадлежность mcyкlic факторам: k•c ∈ (k•g).cycleFactorsFinset эквивалентно c ∈ g.cycleFactorsFinset.

LaTeX

$$theorem mem_cycleFactorsFinset_conj' (k : ConjAct (Perm α)) (g c : Perm α) : k • c ∈ (k • g).cycleFactorsFinset ↔ c ∈ g.cycleFactorsFinset$$

Lean4

/-- A permutation `c` is a cycle of `g` iff `k • c` is a cycle of `k • g` -/
@[simp]
theorem mem_cycleFactorsFinset_conj' (k : ConjAct (Perm α)) (g c : Perm α) :
    k • c ∈ (k • g).cycleFactorsFinset ↔ c ∈ g.cycleFactorsFinset :=
  by
  simp only [ConjAct.smul_def]
  apply mem_cycleFactorsFinset_conj g k

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