sum_const'

Mathlib.SetTheory.Cardinal.Defs

URI: https://scilib.ai/kg/mathlib#Cardinal.sum_const'

English

Let I be an index type and a be a cardinal. Then the sum over i in I of a equals |I| times a.

Русский

Пусть I — тип индексов, а — кардинал. Тогда сумма по i из I от a равна |I| умножить на a.

LaTeX

$$$ \sum_{i : \iota} a = |\iota| \cdot a $$$

Lean4

theorem sum_const' (ι : Type u) (a : Cardinal.{u}) : (sum fun _ : ι => a) = #ι * a := by simp

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

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

Разделы

Аффилиация

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