card_fin

Mathlib.Data.FinEnum

URI: https://scilib.ai/kg/mathlib#FinEnum.card_fin

English

The cardinality of Fin n equals n.

Русский

Число элементов Fin n равно n.

LaTeX

$$$ \\operatorname{card}(\\\\mathrm{Fin}(n)) = n. $$$

Lean4

@[simp]
theorem card_fin {n} [FinEnum (Fin n)] : card (Fin n) = n :=
  Fin.equiv_iff_eq.mp ⟨equiv.symm⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru