nat_card_centralizer_nat_card_stabilizer

English

For any g ∈ G, the cardinality of the centralizer of {g} equals the cardinality of the stabilizer of g under the conjugation action.

Русский

Для любого g ∈ G количество элементов в центральизаторе {g} равно размеру стабилизатора элемента g при действии сопряжения.

LaTeX

$$$\left|\operatorname{centralizer}(\{g\})\right| = \left|\operatorname{Stab}_{\operatorname{ConjAct}(G)}(g)\right|.$$$

Lean4

theorem nat_card_centralizer_nat_card_stabilizer (g : G) :
    Nat.card (centralizer { g }) = Nat.card (MulAction.stabilizer (ConjAct G) g) := by
  rw [centralizer_eq_comap_stabilizer]; rfl

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