mem_ker_toPermHom_iff — Mathlib

English

An element k of the centralizer lies in the kernel of the homomorphism toPermHom g iff k commutes with every cycle factor of g.

Русский

Элемент k центральизатора лежит в ядре гомоморфизма toPermHom g тогда и только тогда, когда k commute c каждым цикл-фактором g.

LaTeX

$$$k \in \ker(toPermHom g) \;\Longleftrightarrow\; \forall c \in g.cycleFactorsFinset,\; Commute(k, c)$$$

Lean4

/-- `k : Subgroup.centralizer {g}` belongs to the kernel of `toPermHom g`
  iff it commutes with each cycle of `g` -/
theorem mem_ker_toPermHom_iff : k ∈ (toPermHom g).ker ↔ ∀ c ∈ g.cycleFactorsFinset, Commute (k : Perm α) c :=
  by
  simp only [toPermHom, MonoidHom.mem_ker, DFunLike.ext_iff, Subtype.forall]
  refine forall₂_congr (fun _ _ ↦ ?_)
  simp [← Subtype.coe_inj, commute_iff_eq, mul_inv_eq_iff_eq_mul]

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