From 29d9631bfe541a745a369cc1ef0e6eb6e0b8e82e Mon Sep 17 00:00:00 2001 From: FM22 Date: Mon, 6 Jan 2025 20:33:52 +0000 Subject: [PATCH] remove spurious deprecation --- Mathlib/Algebra/Ring/Semireal/Defs.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/Mathlib/Algebra/Ring/Semireal/Defs.lean b/Mathlib/Algebra/Ring/Semireal/Defs.lean index e3a694c1ec902..2f6d8609a6e9d 100644 --- a/Mathlib/Algebra/Ring/Semireal/Defs.lean +++ b/Mathlib/Algebra/Ring/Semireal/Defs.lean @@ -35,8 +35,6 @@ class IsSemireal [Add R] [Mul R] [One R] [Zero R] : Prop where add_one_ne_zero_of_isSumSq {a : R} (ssa : IsSumSq a) : 1 + a ≠ 0 @[deprecated (since := "2024-08-09")] alias isSemireal := IsSemireal -@[deprecated (since := "2024-08-09")] alias isSemireal.neg_one_not_SumSq := - IsSemireal.add_one_ne_zero_of_isSumSq theorem IsSemireal.not_isSumSq_neg_one {R : Type*} [AddGroup R] [One R] [Mul R] [IsSemireal R]: ¬ IsSumSq (-1 : R) := (by simpa using add_one_ne_zero_of_isSumSq ·)