card_eq_sum_ones

Mathlib.Data.Fintype.BigOperators

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

English

For a finite type α, the cardinality of α equals the sum over all elements a of α of 1.

Русский

Для конечного множества α кардинальность α равна сумме по всем элементам a ∈ α единицы.

LaTeX

$$$|\\alpha| = \\sum_{a \\in \\mathrm{univ}} 1$$$

Lean4

theorem card_eq_sum_ones {α} [Fintype α] : Fintype.card α = ∑ _a : α, 1 :=
  Finset.card_eq_sum_ones _

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

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

Разделы

Аффилиация

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