orbit_of_normal — Mathlib

English

An orbit of a normal subgroup is itself a block for the G-action.

Русский

Орбита нормальной подгруппы является блоком для действия G.

LaTeX

$$$\\text{IsBlock}(G, \\operatorname{orbit}_N(a))$$$

Lean4

/-- An orbit of a normal subgroup is a block -/
@[to_additive /-- An orbit of a normal subgroup is a block -/
    ]
theorem orbit_of_normal {N : Subgroup G} [N.Normal] (a : X) : IsBlock G (orbit N a) :=
  by
  rw [isBlock_iff_smul_eq_or_disjoint]
  intro g
  rw [smul_orbit_eq_orbit_smul]
  apply orbit.eq_or_disjoint

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