add — Mathlib

English

If s1 and s2 are sums of squares, then s1 + s2 is a sum of squares.

Русский

Если s1 и s2 являются суммами квадратов, то s1 + s2 тоже является суммой квадратов.

LaTeX

$$IsSumSq(s1) ∧ IsSumSq(s2) → IsSumSq(s1 + s2)$$

Lean4

/-- In an additive monoid with multiplication,
if `s₁` and `s₂` are sums of squares, then `s₁ + s₂` is a sum of squares.
-/
@[aesop unsafe 90% apply]
theorem add [AddMonoid R] [Mul R] {s₁ s₂ : R} (h₁ : IsSumSq s₁) (h₂ : IsSumSq s₂) : IsSumSq (s₁ + s₂) := by
  induction h₁ <;> simp_all [add_assoc, sq_add]

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