Theorem IsSumSq.nonneg

Modification history

2025-04-04 17:16
Mathlib/Algebra/Ring/SumsOfSquares.lean
chore: use mixin ordered algebraic typeclasses (part 1) (#20594)
Modified IsSumSq.nonnegView on Github →
2025-01-07 17:42
Mathlib/Algebra/Ring/SumsOfSquares.lean
chore(Algebra/Ring): Clean up in SumsOfSquares and Semireal/Defs (#20528) …
Modified IsSumSq.nonnegView on Github →
2024-08-09 03:04
Mathlib/Algebra/Ring/SumsOfSquares.lean
chore(Algebra/Ring/SumsOfSquares, Algebra/Ring/Semireal): name convension (#15621)
Added IsSumSq.nonnegView on Github →