card_eq_coe_fintype_card — Mathlib

English

If α is a finite type, then ENat.card α equals the finite cardinal of α viewed as an ENat value, i.e. ENat.card α = (Fintype.card α).cast.

Русский

Если α — конечный тип, тогда ENat.card α равно кардиналу α, приведённому к ENat, то есть ENat.card α = (Fintype.card α).cast.

LaTeX

$$$\operatorname{ENat}.card(\alpha) = (\mathrm{Fintype.card}(\alpha)).cast$$$

Lean4

@[simp]
theorem card_eq_coe_fintype_card [Fintype α] : card α = Fintype.card α := by simp [card]

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