sum_sq

Mathlib.Algebra.Ring.SumsOfSquares

URI: https://scilib.ai/kg/mathlib#IsSumSq.sum_sq

English

Over a CommSemiring, the sum of squares is a sum of squares: IsSumSq(∑ i∈I a_i^2).

Русский

В коммутативной полукольце сумма квадратов есть сумма квадратов: IsSumSq(∑_{i∈I} a_i^2).

LaTeX

$$$\\mathrm{IsSumSq}\\left(\\sum_{i \\in I} a_i^2\\right)$$$

Lean4

@[simp↓]
theorem sum_sq [CommSemiring R] {ι : Type*} (I : Finset ι) (a : ι → R) : IsSumSq (∑ i ∈ I, a i ^ 2) := by aesop

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

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

Разделы

Аффилиация

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