sumsq — Mathlib

English

For every a, (1 : Poly α) a = 1.

Русский

Для каждого a верно, что (1 : Poly α) a = 1.

LaTeX

$$$$ (1 : Poly \\alpha)(a) = 1 $$$$

Lean4

/-- The sum of squares of a list of polynomials. This is relevant for
  Diophantine equations, because it means that a list of equations
  can be encoded as a single equation: `x = 0 ∧ y = 0 ∧ z = 0` is
  equivalent to `x^2 + y^2 + z^2 = 0`. -/
def sumsq : List (Poly α) → Poly α
  | [] => 0
  | p :: ps => p * p + sumsq ps

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