nat_card_ofStabilizer_add_one_eq — Mathlib

English

A natural-number version of the fixed-subgroup cardinality relation: ENat.card(FixSub) + 1 = ENat.card(α).

Русский

Натуральная версия кардинальности фиксационной подгруппы: ENat.card(FixSub) + 1 = ENat.card(α).

LaTeX

$$$\mathrm{ENat\_card\_ofStabilizer\_add\_one\_eq}(a):\ ENat.card(\mathrm{ofStabilizer}(G,a)) + 1 = ENat.card(\alpha)$$$

Lean4

@[to_additive]
theorem nat_card_ofStabilizer_add_one_eq [Finite α] (a : α) : Nat.card (ofStabilizer G a) + 1 = Nat.card α :=
  by
  dsimp only [Nat.card]
  rw [← Cardinal.mk_sum_compl { a }, Cardinal.toNat_add Cardinal.mk_lt_aleph0 Cardinal.mk_lt_aleph0]
  simp only [Cardinal.mk_fintype, Fintype.card_unique, Nat.cast_one, map_one, add_comm]
  congr

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