From c17bf63507c8fd5b5e3b371a6549606a5395e7ae Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= Date: Fri, 11 Oct 2024 23:53:30 -0600 Subject: [PATCH] deprecations --- Mathlib/SetTheory/Surreal/Basic.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/Mathlib/SetTheory/Surreal/Basic.lean b/Mathlib/SetTheory/Surreal/Basic.lean index a8c2cc9c505b6..f0a8be3f32e17 100644 --- a/Mathlib/SetTheory/Surreal/Basic.lean +++ b/Mathlib/SetTheory/Surreal/Basic.lean @@ -244,6 +244,12 @@ theorem insertRight {x x' : PGame} (x_num : x.Numeric) (x'_num : x'.Numeric) end Numeric +@[deprecated Numeric.insertLeft (since := "2024-10-11")] +alias insertLeft_numeric := Numeric.insertLeft + +@[deprecated Numeric.insertRight (since := "2024-10-11")] +alias insertRight_numeric := Numeric.insertRight + /-- Pre-games defined by natural numbers are numeric. -/ theorem numeric_nat : ∀ n : ℕ, Numeric n | 0 => numeric_zero