Sums of squares

Copyright (c) 2023 Matematiflo. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Florent Schaffhauser.

This site is live at https://matematiflo.github.io/SumsOfSquares.

We introduce sums of squares and prove some of their basic properties.

The basic setup is that of a general semiring R. For example, we can consider sums of squares of natural numbers (R = ℕ).

For some results, we specialize to rings or fields.

Contents

• Definitions and examples
• Basic properties for lists
• The type of sums of squares
• Some exercises

GitHub repository

The SumsOfSquares repo (Lean package).