sum_const_nat

Mathlib.Algebra.BigOperators.Group.Finset.Basic

URI: https://scilib.ai/kg/mathlib#Finset.sum_const_nat

← MathLib Explorer

English

If f is constant m on s, then the sum over s of f equals #s · m.

Русский

Если f принимает одно и то же значение m на s, то сумма по s равна #s · m.

LaTeX

$$$$\\sum_{x \\in s} f(x) = \\#s \\cdot m$$$$

Lean4

theorem sum_const_nat {m : ℕ} {f : ι → ℕ} (h₁ : ∀ x ∈ s, f x = m) : ∑ x ∈ s, f x = #s * m :=
  by
  rw [← Nat.nsmul_eq_mul, ← sum_const]
  apply sum_congr rfl h₁

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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