card_eq_nat_card — Mathlib

English

For any finite type α, Fintype.card α equals Nat.card α.

Русский

Для любого конечного типа α, Fintype.card α равно Nat.card α.

LaTeX

$$Fintype.card(\\alpha) = Nat.card(\\alpha)$$

Lean4

/-- Because this theorem takes `Fintype α` as a non-instance argument, it can be used in particular
when `Fintype.card` ends up with different instance than the one found by inference -/
theorem _root_.Fintype.card_eq_nat_card {_ : Fintype α} : Fintype.card α = Nat.card α :=
  mk_toNat_eq_card.symm

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