ENat_card_ofStabilizer_add_one_eq

English

Construction of the action of a stabilizer on the complement of a point.

Русский

Построение действия стабилизатора на дополнении точки.

LaTeX

$$$\mathrm{ofStabilizer}(G,a) : \mathrm{SubMulAction} (\mathrm{stabilizer\ G\ a})\ a$$$

Lean4

@[to_additive]
theorem ENat_card_ofStabilizer_add_one_eq (a : α) : ENat.card (ofStabilizer G a) + 1 = ENat.card α :=
  by
  dsimp only [ENat.card]
  rw [← Cardinal.mk_sum_compl { a }, map_add, add_comm, eq_comm]
  congr
  simp

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