index_of_fixingSubgroup_eq — Mathlib

English

For IsMultiplyPretransitive on α with s ⊆ α and hMk: IsMultiplyPretransitive G α s.ncard, we have (fixingSubgroup G s).index = choose(|α|, s.ncard) · s.ncard!.

Русский

При наличии IsMultiplyPretransitive на α с подмножством s ⊆ α и hMk: IsMultiplyPretransitive G α |s|, индекс фиксирующей подгруппы равен C(|α|, |s|) · |s|!.

LaTeX

$$$(fixingSubgroup G s).index = \binom{|α|}{|s|} \; |s|!$$$

Lean4

/-- For a multiply pretransitive action,
computes the index of the `fixingSubgroup` of a subset
of adequate cardinality. -/
theorem index_of_fixingSubgroup_eq [Finite α] (s : Set α) (hMk : IsMultiplyPretransitive G α s.ncard) :
    (fixingSubgroup G s).index = Nat.choose (Nat.card α) s.ncard * s.ncard.factorial :=
  by
  apply Nat.eq_of_mul_eq_mul_right (Nat.factorial_pos _)
  rw [hMk.index_of_fixingSubgroup_mul rfl, Nat.choose_mul_factorial_mul_factorial]
  rw [← ncard_univ]
  exact ncard_le_ncard (subset_univ s)

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