Commit 2024-08-09 03:04 bc37ac3c

View on Github →

chore(Algebra/Ring/SumsOfSquares, Algebra/Ring/Semireal): name convension (#15621)

Estimated changes

added theorem IsSumSq.add
added theorem IsSumSq.nonneg
added inductive IsSumSq
deleted theorem SquaresAddClosure
deleted theorem SquaresInSumSq
deleted def SumSqIn
deleted theorem isSumSq.add
deleted theorem isSumSq.nonneg
deleted inductive isSumSq
added def sumSqIn