From ad2ba3a9674da18e41de4dada830ca6371823ae1 Mon Sep 17 00:00:00 2001 From: FM22 Date: Mon, 6 Jan 2025 20:00:07 +0000 Subject: [PATCH] style --- Mathlib/Algebra/Ring/SumsOfSquares.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Algebra/Ring/SumsOfSquares.lean b/Mathlib/Algebra/Ring/SumsOfSquares.lean index 773350cbd2004..766ef302e00ee 100644 --- a/Mathlib/Algebra/Ring/SumsOfSquares.lean +++ b/Mathlib/Algebra/Ring/SumsOfSquares.lean @@ -204,7 +204,7 @@ sums of squares are non-negative. theorem IsSumSq.nonneg {R : Type*} [LinearOrderedSemiring R] [ExistsAddOfLE R] {s : R} (hs : IsSumSq s) : 0 ≤ s := by induction ps using IsSumSq.rec' - case zero => aesop - case sq_add x s hx hs h_sum => exact add_nonneg (IsSquare.nonneg hx) h_sum + | zero => aesop + | sq_add x s hx hs h_sum => exact add_nonneg (IsSquare.nonneg hx) h_sum @[deprecated (since := "2024-08-09")] alias isSumSq.nonneg := IsSumSq.nonneg