ncard_block_eq_relIndex — Mathlib

English

For B a block and x ∈ B, the number of elements in B equals the index of the stabilizer of x in the stabilizer of B.

Русский

Для блока B и x ∈ B число элементов B равно индексу стабилизатора x внутри стабилизатора B.

LaTeX

$$B.ncard = (stabilizer G x).relIndex (stabilizer G B)$$

Lean4

@[to_additive]
theorem ncard_block_eq_relIndex (hB : IsBlock G B) {x : X} (hx : x ∈ B) :
    B.ncard = (stabilizer G x).relIndex (stabilizer G B) :=
  by
  have key : (stabilizer G x).subgroupOf (stabilizer G B) = stabilizer (stabilizer G B) x := by ext; rfl
  rw [Subgroup.relIndex, key, index_stabilizer, hB.orbit_stabilizer_eq hx]

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