nat_card_ofStabilizer_eq — Mathlib

English

If Finite α holds, then Nat.card(ofStabilizer G a) = Nat.card α − 1.

Русский

Если множество α конечно, то Nat.card(ofStabilizer G a) = Nat.card α − 1.

LaTeX

$$$\mathrm{nat\_card\_ofStabilizer\_eq}\ M a: \mathrm{Nat.card}(\mathrm{ofStabilizer}(G,a)) = \mathrm{Nat.card}(\alpha) - 1$$$

Lean4

@[to_additive]
theorem nat_card_ofStabilizer_eq [Finite α] (a : α) : Nat.card (ofStabilizer G a) = Nat.card α - 1 :=
  Nat.eq_sub_of_add_eq (nat_card_ofStabilizer_add_one_eq G a)

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