English
Let R be an additive monoid with multiplication. The submonoid generated by the squares is exactly the set of sums of squares in R; equivalently, closure { x in R | IsSquare x } equals sumSq R.
Русский
Пусть R — добавочно-монойд с умножением. Подмножество, сгенерированное квадратами, совпадает с подмножеством сумм квадратов в R; то есть closure { x ∈ R | IsSquare(x) } = sumSq R.
LaTeX
$$$\operatorname{closure}\{ x : R \mid \operatorname{IsSquare}(x) \} = \operatorname{sumSq} R$$$
Lean4
/-- In an additive monoid with multiplication `R`, the submonoid generated by the squares is the set of
sums of squares in `R`.
-/
@[simp]
theorem closure_isSquare [AddMonoid R] [Mul R] : closure {x : R | IsSquare x} = sumSq R :=
by
refine closure_eq_of_le (fun x hx ↦ IsSquare.isSumSq hx) (fun x hx ↦ ?_)
induction hx <;> aesop
