card

Mathlib.Data.Fintype.Card

URI: https://scilib.ai/kg/mathlib#Fintype.card

English

For a finite type α, the function card(α) returns the number of elements of α.

Русский

Для конечного типа α функция card(α) возвращает количество элементов α.

LaTeX

$$$ \\operatorname{card}(\\alpha) = |\\alpha|\\quad \\text{(finite } \\alpha\\text{)}$$$

Lean4

/-- `card α` is the number of elements in `α`, defined when `α` is a fintype. -/
def card (α) [Fintype α] : ℕ :=
  (@univ α _).card

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

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

Разделы

Аффилиация

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