isSumSq — Mathlib

English

If x is a square in an additive unital magma with multiplication, then x is a sum of squares.

Русский

Если x является квадратом в аддитивной однородной полугруппе с умножением, то x — сумма квадратов.

LaTeX

$$IsSquare(x) → IsSumSq(x)$$

Lean4

/-- In an additive unital magma with multiplication, squares are sums of squares
(see Mathlib.Algebra.Group.Even).
-/
@[aesop unsafe 80% apply]
theorem isSumSq [AddZeroClass R] [Mul R] {x : R} (hx : IsSquare x) : IsSumSq x := by aesop

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