From 588d5b9e006b7f948bd9fbdd6c71012dd3719d7a Mon Sep 17 00:00:00 2001 From: grunweg Date: Wed, 24 Apr 2024 05:40:44 +0000 Subject: [PATCH] chore: unify date formatting in lemma deprecations (#12334) - consistently use the YYYY-MM-DD format - when easily possible, put the date on the same line as the `deprecated` attribute - when easily possible, format the entire declaration on the same line Why these changes? - consistency makes it easier for tools to parse this information - compactness: I don't see a good reason for these declarations taking up more space than needed; as I understand it, deprecated lemmas are not supposed to be used in mathlib anyway - putting the date on the same line as the attribute makes it easier to discover un-dated deprecations; they also ease writing a tool to replace these by a machine-readable version using leanprover/lean4#3968 --- Mathlib/Algebra/Associated.lean | 2 +- Mathlib/Algebra/BigOperators/Basic.lean | 10 ++-------- Mathlib/Algebra/Group/Units.lean | 2 +- Mathlib/Algebra/Lie/Weights/Linear.lean | 4 ++-- Mathlib/Algebra/Module/Basic.lean | 3 ++- .../Algebra/Order/BigOperators/Ring/Finset.lean | 3 +-- Mathlib/Algebra/Order/Ring/Defs.lean | 7 +------ Mathlib/Algebra/Polynomial/Div.lean | 3 +-- .../Calculus/InverseFunctionTheorem/FDeriv.lean | 4 ++-- Mathlib/Analysis/Fourier/FourierTransform.lean | 8 ++++---- Mathlib/Analysis/InnerProductSpace/TwoDim.lean | 2 +- Mathlib/Analysis/LocallyConvex/Basic.lean | 8 +++----- Mathlib/Analysis/LocallyConvex/Bounded.lean | 2 +- Mathlib/Analysis/NormedSpace/FiniteDimension.lean | 10 +++++----- .../Analysis/NormedSpace/Multilinear/Basic.lean | 4 +--- .../Gaussian/FourierTransform.lean | 11 +++++------ Mathlib/Analysis/SpecialFunctions/Pow/Real.lean | 8 +------- Mathlib/Data/Complex/Abs.lean | 4 ++-- Mathlib/Data/ENNReal/Basic.lean | 7 +------ Mathlib/Data/Finset/Card.lean | 8 +------- Mathlib/Data/Finset/Image.lean | 10 ++-------- Mathlib/Data/Int/Defs.lean | 4 ++-- Mathlib/Data/Int/ModEq.lean | 3 +-- Mathlib/Data/Multiset/Basic.lean | 10 ++-------- Mathlib/Data/NNRat/Defs.lean | 3 +-- Mathlib/Data/Nat/Digits.lean | 9 +++------ Mathlib/Data/Rat/Defs.lean | 14 ++++++-------- Mathlib/Data/Real/NNReal.lean | 3 +-- Mathlib/Data/Subtype.lean | 3 +-- Mathlib/Data/ZMod/Quotient.lean | 5 +++-- Mathlib/Deprecated/Submonoid.lean | 2 +- Mathlib/FieldTheory/PrimitiveElement.lean | 4 ++-- Mathlib/LinearAlgebra/FiniteDimensional.lean | 6 +++--- Mathlib/Logic/Function/Conjugate.lean | 2 +- Mathlib/MeasureTheory/Function/L1Space.lean | 6 ++---- Mathlib/MeasureTheory/Function/SimpleFunc.lean | 3 +-- .../Function/StronglyMeasurable/Basic.lean | 2 +- Mathlib/RingTheory/UniqueFactorizationDomain.lean | 2 +- Mathlib/Topology/Bases.lean | 4 ++-- Mathlib/Topology/CompactOpen.lean | 2 +- Mathlib/Topology/MetricSpace/ProperSpace.lean | 2 +- Mathlib/Topology/Order.lean | 4 ++-- 42 files changed, 78 insertions(+), 135 deletions(-) diff --git a/Mathlib/Algebra/Associated.lean b/Mathlib/Algebra/Associated.lean index c79184c1137527..085e7a3e21d10e 100644 --- a/Mathlib/Algebra/Associated.lean +++ b/Mathlib/Algebra/Associated.lean @@ -1026,7 +1026,7 @@ theorem isPrimal_mk {a : α} : IsPrimal (Associates.mk a) ↔ IsPrimal a := by exact ⟨a₁, a₂ * u, h₁, Units.mul_right_dvd.mpr h₂, mul_assoc _ _ _⟩ · exact ⟨a₁, a₂, h₁, h₂, congr_arg _ eq⟩ -@[deprecated] alias isPrimal_iff := isPrimal_mk -- 2024/03/16 +@[deprecated] alias isPrimal_iff := isPrimal_mk -- 2024-03-16 @[simp] theorem decompositionMonoid_iff : DecompositionMonoid (Associates α) ↔ DecompositionMonoid α := by diff --git a/Mathlib/Algebra/BigOperators/Basic.lean b/Mathlib/Algebra/BigOperators/Basic.lean index 7c689e9799e296..5a51fe6edf8cac 100644 --- a/Mathlib/Algebra/BigOperators/Basic.lean +++ b/Mathlib/Algebra/BigOperators/Basic.lean @@ -2499,11 +2499,5 @@ theorem toAdd_prod (s : Finset ι) (f : ι → Multiplicative α) : end AddCommMonoid -/-! -### Deprecated lemmas - -Those lemmas were deprecated on the 2023/12/23. --/ - -@[deprecated] alias Equiv.prod_comp' := Fintype.prod_equiv -@[deprecated] alias Equiv.sum_comp' := Fintype.sum_equiv +@[deprecated] alias Equiv.prod_comp' := Fintype.prod_equiv -- 2023-12-23 +@[deprecated] alias Equiv.sum_comp' := Fintype.sum_equiv -- 2023-12-23 diff --git a/Mathlib/Algebra/Group/Units.lean b/Mathlib/Algebra/Group/Units.lean index 7d0a07bc4cd248..97acf6fcf60fa4 100644 --- a/Mathlib/Algebra/Group/Units.lean +++ b/Mathlib/Algebra/Group/Units.lean @@ -1214,7 +1214,7 @@ noncomputable def commGroupOfIsUnit [hM : CommMonoid M] (h : ∀ a : M, IsUnit a end NoncomputableDefs --- 2024--03-20 +-- 2024-03-20 attribute [deprecated div_mul_cancel_right] IsUnit.div_mul_left attribute [deprecated sub_add_cancel_right] IsAddUnit.sub_add_left attribute [deprecated div_mul_cancel_left] IsUnit.div_mul_right diff --git a/Mathlib/Algebra/Lie/Weights/Linear.lean b/Mathlib/Algebra/Lie/Weights/Linear.lean index 7f37c878bd796a..3f701f36f15b52 100644 --- a/Mathlib/Algebra/Lie/Weights/Linear.lean +++ b/Mathlib/Algebra/Lie/Weights/Linear.lean @@ -125,8 +125,8 @@ lemma trace_comp_toEndomorphism_weightSpace_eq (χ : L → R) : rw [LinearMap.comp_apply, LieHom.coe_toLinearMap, h₁, map_add, h₂] simp [mul_comm (χ x)] -@[deprecated] alias trace_comp_toEndomorphism_weight_space_eq := - trace_comp_toEndomorphism_weightSpace_eq -- 2024-04-06 +@[deprecated] -- 2024-04-06 +alias trace_comp_toEndomorphism_weight_space_eq := trace_comp_toEndomorphism_weightSpace_eq variable {R L M} in lemma zero_lt_finrank_weightSpace {χ : L → R} (hχ : weightSpace M χ ≠ ⊥) : diff --git a/Mathlib/Algebra/Module/Basic.lean b/Mathlib/Algebra/Module/Basic.lean index 4d33f41dec0fe3..2611a70d2b788e 100644 --- a/Mathlib/Algebra/Module/Basic.lean +++ b/Mathlib/Algebra/Module/Basic.lean @@ -105,7 +105,8 @@ theorem two_smul : (2 : R) • x = x + x := by rw [← one_add_one_eq_two, add_s #align two_smul two_smul set_option linter.deprecated false in -@[deprecated] theorem two_smul' : (2 : R) • x = bit0 x := +@[deprecated] +theorem two_smul' : (2 : R) • x = bit0 x := two_smul R x #align two_smul' two_smul' diff --git a/Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean b/Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean index c6236f42648f73..1c8f13e1aa0a17 100644 --- a/Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean +++ b/Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean @@ -191,8 +191,7 @@ lemma IsAbsoluteValue.abv_sum [Semiring R] [OrderedSemiring S] (abv : R → S) [ (IsAbsoluteValue.toAbsoluteValue abv).sum_le _ _ #align is_absolute_value.abv_sum IsAbsoluteValue.abv_sum --- 2024-02-14 -@[deprecated] alias abv_sum_le_sum_abv := IsAbsoluteValue.abv_sum +@[deprecated] alias abv_sum_le_sum_abv := IsAbsoluteValue.abv_sum -- 2024-02-14 nonrec lemma AbsoluteValue.map_prod [CommSemiring R] [Nontrivial R] [LinearOrderedCommRing S] (abv : AbsoluteValue R S) (f : ι → R) (s : Finset ι) : diff --git a/Mathlib/Algebra/Order/Ring/Defs.lean b/Mathlib/Algebra/Order/Ring/Defs.lean index 33b3f859fdd3b5..17c5cb9ac88b60 100644 --- a/Mathlib/Algebra/Order/Ring/Defs.lean +++ b/Mathlib/Algebra/Order/Ring/Defs.lean @@ -1325,12 +1325,7 @@ instance (priority := 100) LinearOrderedCommRing.toLinearOrderedCommSemiring { d, LinearOrderedRing.toLinearOrderedSemiring with } #align linear_ordered_comm_ring.to_linear_ordered_comm_semiring LinearOrderedCommRing.toLinearOrderedCommSemiring -/-! -### Deprecated lemmas - -Those lemmas have been deprecated on 2023/12/23 --/ - +-- 2023-12-23 @[deprecated] alias zero_le_mul_left := mul_nonneg_iff_of_pos_left @[deprecated] alias zero_le_mul_right := mul_nonneg_iff_of_pos_right @[deprecated] alias zero_lt_mul_left := mul_pos_iff_of_pos_left diff --git a/Mathlib/Algebra/Polynomial/Div.lean b/Mathlib/Algebra/Polynomial/Div.lean index 40c49c070d97b9..99102ca84e12c6 100644 --- a/Mathlib/Algebra/Polynomial/Div.lean +++ b/Mathlib/Algebra/Polynomial/Div.lean @@ -412,8 +412,7 @@ theorem modByMonic_eq_zero_iff_dvd (hq : Monic q) : p %ₘ q = 0 ↔ q ∣ p := exact not_lt_of_ge (Nat.le_add_right _ _) (WithBot.some_lt_some.1 this)⟩ #align polynomial.dvd_iff_mod_by_monic_eq_zero Polynomial.modByMonic_eq_zero_iff_dvd --- 2024-03-23 -@[deprecated] alias dvd_iff_modByMonic_eq_zero := modByMonic_eq_zero_iff_dvd +@[deprecated] alias dvd_iff_modByMonic_eq_zero := modByMonic_eq_zero_iff_dvd -- 2024-03-23 /-- See `Polynomial.mul_left_modByMonic` for the other multiplication order. That version, unlike this one, requires commutativity. -/ diff --git a/Mathlib/Analysis/Calculus/InverseFunctionTheorem/FDeriv.lean b/Mathlib/Analysis/Calculus/InverseFunctionTheorem/FDeriv.lean index 80d31a5934dd00..3ede670a850c68 100644 --- a/Mathlib/Analysis/Calculus/InverseFunctionTheorem/FDeriv.lean +++ b/Mathlib/Analysis/Calculus/InverseFunctionTheorem/FDeriv.lean @@ -217,5 +217,5 @@ theorem isOpenMap_of_hasStrictFDerivAt_equiv [CompleteSpace E] {f : E → F} {f' (hf : ∀ x, HasStrictFDerivAt f (f' x : E →L[𝕜] F) x) : IsOpenMap f := isOpenMap_iff_nhds_le.2 fun x => (hf x).map_nhds_eq_of_equiv.ge #align open_map_of_strict_fderiv_equiv isOpenMap_of_hasStrictFDerivAt_equiv -@[deprecated] alias open_map_of_strict_fderiv_equiv := - isOpenMap_of_hasStrictFDerivAt_equiv -- 2024-03-23 +@[deprecated] -- 2024-03-23 +alias open_map_of_strict_fderiv_equiv := isOpenMap_of_hasStrictFDerivAt_equiv diff --git a/Mathlib/Analysis/Fourier/FourierTransform.lean b/Mathlib/Analysis/Fourier/FourierTransform.lean index eb5febc156bdb1..eee3cacd455ed3 100644 --- a/Mathlib/Analysis/Fourier/FourierTransform.lean +++ b/Mathlib/Analysis/Fourier/FourierTransform.lean @@ -147,8 +147,8 @@ theorem fourierIntegral_convergent_iff (he : Continuous e) exact this #align vector_fourier.fourier_integral_convergent_iff VectorFourier.fourierIntegral_convergent_iff -@[deprecated] alias fourier_integral_convergent_iff := - VectorFourier.fourierIntegral_convergent_iff -- 2024-03-29 +@[deprecated] -- 2024-03-29 +alias fourier_integral_convergent_iff := VectorFourier.fourierIntegral_convergent_iff variable [CompleteSpace E] @@ -463,8 +463,8 @@ theorem fourierIntegral_real_eq_integral_exp_smul (f : ℝ → E) (w : ℝ) : mul_assoc] #align real.fourier_integral_eq_integral_exp_smul Real.fourierIntegral_real_eq_integral_exp_smul -@[deprecated] alias fourierIntegral_eq_integral_exp_smul := - fourierIntegral_real_eq_integral_exp_smul -- deprecated on 2024-02-21 +@[deprecated] -- deprecated on 2024-02-21 +alias fourierIntegral_eq_integral_exp_smul := fourierIntegral_real_eq_integral_exp_smul @[simp] theorem fourierIntegral_convergent_iff {μ : Measure V} {f : V → E} (w : V) : Integrable (fun v : V ↦ 𝐞 (- ⟪v, w⟫) • f v) μ ↔ Integrable f μ := diff --git a/Mathlib/Analysis/InnerProductSpace/TwoDim.lean b/Mathlib/Analysis/InnerProductSpace/TwoDim.lean index 10b7ddfd1cf562..5f55806cb3a4c5 100644 --- a/Mathlib/Analysis/InnerProductSpace/TwoDim.lean +++ b/Mathlib/Analysis/InnerProductSpace/TwoDim.lean @@ -80,7 +80,7 @@ lemma FiniteDimensional.of_fact_finrank_eq_two {K V : Type*} [DivisionRing K] attribute [local instance] FiniteDimensional.of_fact_finrank_eq_two -@[deprecated] -- Since 2024/02/02 +@[deprecated] -- Since 2024-02-02 alias FiniteDimensional.finiteDimensional_of_fact_finrank_eq_two := FiniteDimensional.of_fact_finrank_eq_two diff --git a/Mathlib/Analysis/LocallyConvex/Basic.lean b/Mathlib/Analysis/LocallyConvex/Basic.lean index 4c0f8e6b113a4c..a42cc95d641a6a 100644 --- a/Mathlib/Analysis/LocallyConvex/Basic.lean +++ b/Mathlib/Analysis/LocallyConvex/Basic.lean @@ -236,8 +236,7 @@ theorem Balanced.smul_mem_iff (hs : Balanced 𝕜 s) (h : ‖a‖ = ‖b‖) : a ⟨(hs.smul_mem_mono · h.ge), (hs.smul_mem_mono · h.le)⟩ #align balanced.mem_smul_iff Balanced.smul_mem_iff -@[deprecated] -- Since 2024/02/02 -alias Balanced.mem_smul_iff := Balanced.smul_mem_iff +@[deprecated] alias Balanced.mem_smul_iff := Balanced.smul_mem_iff -- since 2024-02-02 variable [TopologicalSpace E] [ContinuousSMul 𝕜 E] @@ -281,7 +280,7 @@ section NontriviallyNormedField variable [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} -@[deprecated Absorbent.zero_mem] -- Since 2024/02/02 +@[deprecated Absorbent.zero_mem] -- Since 2024-02-02 theorem Absorbent.zero_mem' (hs : Absorbent 𝕜 s) : (0 : E) ∈ s := hs.zero_mem variable [Module ℝ E] [SMulCommClass ℝ 𝕜 E] @@ -296,8 +295,7 @@ protected theorem Balanced.convexHull (hs : Balanced 𝕜 s) : Balanced 𝕜 (co exact convex_convexHull ℝ s (hx a ha) (hy a ha) hu hv huv #align balanced_convex_hull_of_balanced Balanced.convexHull -@[deprecated] -- Since 2024/02/02 -alias balanced_convexHull_of_balanced := Balanced.convexHull +@[deprecated] alias balanced_convexHull_of_balanced := Balanced.convexHull -- Since 2024-02-02 end NontriviallyNormedField diff --git a/Mathlib/Analysis/LocallyConvex/Bounded.lean b/Mathlib/Analysis/LocallyConvex/Bounded.lean index e9f8589bbbb64d..50b4bbed03789b 100644 --- a/Mathlib/Analysis/LocallyConvex/Bounded.lean +++ b/Mathlib/Analysis/LocallyConvex/Bounded.lean @@ -84,7 +84,7 @@ theorem _root_.Filter.HasBasis.isVonNBounded_iff {q : ι → Prop} {s : ι → S exact (hA i hi).mono_left hV #align filter.has_basis.is_vonN_bounded_basis_iff Filter.HasBasis.isVonNBounded_iff -@[deprecated] -- since 12 January 2024 +@[deprecated] -- since 2024-01-12 alias _root_.Filter.HasBasis.isVonNBounded_basis_iff := Filter.HasBasis.isVonNBounded_iff /-- Subsets of bounded sets are bounded. -/ diff --git a/Mathlib/Analysis/NormedSpace/FiniteDimension.lean b/Mathlib/Analysis/NormedSpace/FiniteDimension.lean index 7c15e90850bdb6..a5806d8d2d03c9 100644 --- a/Mathlib/Analysis/NormedSpace/FiniteDimension.lean +++ b/Mathlib/Analysis/NormedSpace/FiniteDimension.lean @@ -493,7 +493,7 @@ theorem FiniteDimensional.of_isCompact_closedBall₀ {r : ℝ} (rpos : 0 < r) _ < ‖c‖ := hN (N + 1) (Nat.le_succ N) #align finite_dimensional_of_is_compact_closed_ball₀ FiniteDimensional.of_isCompact_closedBall₀ -@[deprecated] -- Since 2024/02/02 +@[deprecated] -- Since 2024-02-02 alias finiteDimensional_of_isCompact_closedBall₀ := FiniteDimensional.of_isCompact_closedBall₀ /-- **Riesz's theorem**: if a closed ball of positive radius is compact in a vector space, then the @@ -503,7 +503,7 @@ theorem FiniteDimensional.of_isCompact_closedBall {r : ℝ} (rpos : 0 < r) {c : .of_isCompact_closedBall₀ 𝕜 rpos <| by simpa using h.vadd (-c) #align finite_dimensional_of_is_compact_closed_ball FiniteDimensional.of_isCompact_closedBall -@[deprecated] -- Since 2024/02/02 +@[deprecated] -- Since 2024-02-02 alias finiteDimensional_of_isCompact_closedBall := FiniteDimensional.of_isCompact_closedBall /-- **Riesz's theorem**: a locally compact normed vector space is finite-dimensional. -/ @@ -512,7 +512,7 @@ theorem FiniteDimensional.of_locallyCompactSpace [LocallyCompactSpace E] : let ⟨_r, rpos, hr⟩ := exists_isCompact_closedBall (0 : E) .of_isCompact_closedBall₀ 𝕜 rpos hr -@[deprecated] -- Since 2024/02/02 +@[deprecated] -- Since 2024-02-02 alias finiteDimensional_of_locallyCompactSpace := FiniteDimensional.of_locallyCompactSpace /-- If a function has compact support, then either the function is trivial @@ -548,7 +548,7 @@ lemma ProperSpace.of_locallyCompactSpace (𝕜 : Type*) [NontriviallyNormedField Tendsto.atTop_mul_const rpos (tendsto_pow_atTop_atTop_of_one_lt hc) exact .of_seq_closedBall hTop (eventually_of_forall hC) -@[deprecated] -- Since 2024/01/31 +@[deprecated] -- Since 2024-01-31 alias properSpace_of_locallyCompactSpace := ProperSpace.of_locallyCompactSpace variable (E) @@ -561,7 +561,7 @@ lemma ProperSpace.of_locallyCompact_module [Nontrivial E] [LocallyCompactSpace E apply ClosedEmbedding.locallyCompactSpace this .of_locallyCompactSpace 𝕜 -@[deprecated] -- Since 2024/01/31 +@[deprecated] -- Since 2024-01-31 alias properSpace_of_locallyCompact_module := ProperSpace.of_locallyCompact_module end Riesz diff --git a/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean b/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean index 21d5c4023440b4..1e396332c1bf02 100644 --- a/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean +++ b/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean @@ -1379,9 +1379,7 @@ theorem opNorm_zero_iff : ‖f‖ = 0 ↔ f = 0 := by simp [← (opNorm_nonneg f).le_iff_eq, opNorm_le_iff f le_rfl, ext_iff] #align continuous_multilinear_map.op_norm_zero_iff ContinuousMultilinearMap.opNorm_zero_iff -@[deprecated] -alias op_norm_zero_iff := - opNorm_zero_iff -- deprecated on 2024-02-02 +@[deprecated] alias op_norm_zero_iff := opNorm_zero_iff -- deprecated on 2024-02-02 /-- Continuous multilinear maps themselves form a normed group with respect to the operator norm. -/ diff --git a/Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean b/Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean index e3d9107beacbad..cccc47a6989ab7 100644 --- a/Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean +++ b/Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean @@ -223,8 +223,7 @@ theorem _root_.fourierIntegral_gaussian (hb : 0 < b.re) (t : ℂ) : mul_neg, div_neg, neg_neg, mul_pow, I_sq, neg_one_mul, mul_comm] #align fourier_transform_gaussian fourierIntegral_gaussian -@[deprecated] alias _root_.fourier_transform_gaussian := - fourierIntegral_gaussian -- deprecated on 2024-02-21 +@[deprecated] alias _root_.fourier_transform_gaussian := fourierIntegral_gaussian -- 2024-02-21 theorem _root_.fourierIntegral_gaussian_pi' (hb : 0 < b.re) (c : ℂ) : (𝓕 fun x : ℝ => cexp (-π * b * x ^ 2 + 2 * π * c * x)) = fun t : ℝ => @@ -246,8 +245,8 @@ theorem _root_.fourierIntegral_gaussian_pi' (hb : 0 < b.re) (c : ℂ) : simp only [I_sq] ring -@[deprecated] alias _root_.fourier_transform_gaussian_pi' := - _root_.fourierIntegral_gaussian_pi' -- deprecated on 2024-02-21 +@[deprecated] -- deprecated on 2024-02-21 +alias _root_.fourier_transform_gaussian_pi' := _root_.fourierIntegral_gaussian_pi' theorem _root_.fourierIntegral_gaussian_pi (hb : 0 < b.re) : (𝓕 fun (x : ℝ) ↦ cexp (-π * b * x ^ 2)) = @@ -255,8 +254,8 @@ theorem _root_.fourierIntegral_gaussian_pi (hb : 0 < b.re) : simpa only [mul_zero, zero_mul, add_zero] using fourierIntegral_gaussian_pi' hb 0 #align fourier_transform_gaussian_pi fourierIntegral_gaussian_pi -@[deprecated] alias root_.fourier_transform_gaussian_pi := - _root_.fourierIntegral_gaussian_pi -- deprecated on 2024-02-21 +@[deprecated] -- 2024-02-21 +alias root_.fourier_transform_gaussian_pi := _root_.fourierIntegral_gaussian_pi section InnerProductSpace diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean b/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean index 008022dcab5a71..2d0e505d83b4ba 100644 --- a/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean +++ b/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean @@ -1051,10 +1051,4 @@ end Mathlib.Meta.NormNum end Tactics -/-! -### Deprecated lemmas - -These lemmas have been deprecated on 2024-01-07. --/ - -@[deprecated] alias rpow_nonneg_of_nonneg := rpow_nonneg +@[deprecated] alias rpow_nonneg_of_nonneg := rpow_nonneg -- 2024-01-07 diff --git a/Mathlib/Data/Complex/Abs.lean b/Mathlib/Data/Complex/Abs.lean index ba17eb5b646aca..6997a66c05f6ed 100644 --- a/Mathlib/Data/Complex/Abs.lean +++ b/Mathlib/Data/Complex/Abs.lean @@ -243,8 +243,8 @@ theorem abs_im_div_abs_le_one (z : ℂ) : |z.im / Complex.abs z| ≤ 1 := @[simp, norm_cast] lemma abs_intCast (n : ℤ) : abs n = |↑n| := by rw [← ofReal_intCast, abs_ofReal] #align complex.int_cast_abs Complex.abs_intCast --- 2024-02-14 -@[deprecated] lemma int_cast_abs (n : ℤ) : |↑n| = Complex.abs n := (abs_intCast _).symm +@[deprecated] -- 2024-02-14 +lemma int_cast_abs (n : ℤ) : |↑n| = Complex.abs n := (abs_intCast _).symm theorem normSq_eq_abs (x : ℂ) : normSq x = (Complex.abs x) ^ 2 := by simp [abs, sq, abs_def, Real.mul_self_sqrt (normSq_nonneg _)] diff --git a/Mathlib/Data/ENNReal/Basic.lean b/Mathlib/Data/ENNReal/Basic.lean index fdcdcb4acd987c..be164ffcae3c9c 100644 --- a/Mathlib/Data/ENNReal/Basic.lean +++ b/Mathlib/Data/ENNReal/Basic.lean @@ -870,11 +870,6 @@ def evalENNRealOfNNReal : PositivityExt where eval {u α} _zα _pα e := do end Mathlib.Meta.Positivity -/-! -### Deprecated lemmas - -Those lemmas have been deprecated on the 2023/12/23. --/ - +-- 2023-12-23 @[deprecated] protected alias ENNReal.le_inv_smul_iff_of_pos := le_inv_smul_iff_of_pos @[deprecated] protected alias ENNReal.inv_smul_le_iff_of_pos := inv_smul_le_iff_of_pos diff --git a/Mathlib/Data/Finset/Card.lean b/Mathlib/Data/Finset/Card.lean index c3b9c7973fd80d..cec27acc77b6fb 100644 --- a/Mathlib/Data/Finset/Card.lean +++ b/Mathlib/Data/Finset/Card.lean @@ -849,12 +849,6 @@ theorem lt_wf {α} : WellFounded (@LT.lt (Finset α) _) := Subrelation.wf H <| InvImage.wf _ <| (Nat.lt_wfRel).2 #align finset.lt_wf Finset.lt_wf -/-! -### Deprecated lemmas - -Those lemmas have been deprecated on 2023-12-27. --/ - -@[deprecated] alias card_le_of_subset := card_le_card +@[deprecated] alias card_le_of_subset := card_le_card -- 2023-12-27 end Finset diff --git a/Mathlib/Data/Finset/Image.lean b/Mathlib/Data/Finset/Image.lean index 6846118b8b7fe5..029d6204d6f542 100644 --- a/Mathlib/Data/Finset/Image.lean +++ b/Mathlib/Data/Finset/Image.lean @@ -435,7 +435,7 @@ protected theorem Nonempty.image (h : s.Nonempty) (f : α → β) : (s.image f). alias ⟨Nonempty.of_image, _⟩ := image_nonempty -@[deprecated image_nonempty] -- Since 29 December 2023 +@[deprecated image_nonempty] -- 2023-12-29 theorem Nonempty.image_iff (f : α → β) : (s.image f).Nonempty ↔ s.Nonempty := image_nonempty @@ -901,14 +901,8 @@ theorem finsetCongr_toEmbedding (e : α ≃ β) : end Equiv -/-! -### Deprecated lemmas - -Those lemmas have been deprecated on 2023-12-27. --/ - namespace Finset -@[deprecated] alias image_filter := filter_image +@[deprecated] alias image_filter := filter_image -- 2023-12-27 end Finset diff --git a/Mathlib/Data/Int/Defs.lean b/Mathlib/Data/Int/Defs.lean index 5d12ff5fe49120..037e07998d2086 100644 --- a/Mathlib/Data/Int/Defs.lean +++ b/Mathlib/Data/Int/Defs.lean @@ -63,8 +63,8 @@ instance instNontrivial : Nontrivial ℤ := ⟨⟨0, 1, Int.zero_ne_one⟩⟩ @[simp] lemma ofNat_eq_natCast : Int.ofNat n = n := rfl --- 2024-03-24 -@[deprecated ofNat_eq_natCast] protected lemma natCast_eq_ofNat (n : ℕ) : ↑n = Int.ofNat n := rfl +@[deprecated ofNat_eq_natCast] -- 2024-03-24 +protected lemma natCast_eq_ofNat (n : ℕ) : ↑n = Int.ofNat n := rfl #align int.coe_nat_eq Int.natCast_eq_ofNat @[norm_cast] lemma natCast_inj : (m : ℤ) = (n : ℤ) ↔ m = n := ofNat_inj diff --git a/Mathlib/Data/Int/ModEq.lean b/Mathlib/Data/Int/ModEq.lean index 0f9872bb4615e8..26da44d0df73c5 100644 --- a/Mathlib/Data/Int/ModEq.lean +++ b/Mathlib/Data/Int/ModEq.lean @@ -325,7 +325,6 @@ theorem mod_mul_left_mod (a b c : ℤ) : a % (b * c) % c = a % c := (mod_modEq _ _).of_mul_left _ #align int.mod_mul_left_mod Int.mod_mul_left_mod --- 2024-04-02 -@[deprecated] alias coe_nat_modEq_iff := natCast_modEq_iff +@[deprecated] alias coe_nat_modEq_iff := natCast_modEq_iff -- 2024-04-02 end Int diff --git a/Mathlib/Data/Multiset/Basic.lean b/Mathlib/Data/Multiset/Basic.lean index 2c89c72cef2f36..40a2fa74f576e1 100644 --- a/Mathlib/Data/Multiset/Basic.lean +++ b/Mathlib/Data/Multiset/Basic.lean @@ -3208,13 +3208,7 @@ theorem coe_subsingletonEquiv [Subsingleton α] : rfl #align multiset.coe_subsingleton_equiv Multiset.coe_subsingletonEquiv -/-! -### Deprecated lemmas - -Those lemmas have been deprecated on 2023-12-27. --/ - -@[deprecated] alias card_le_of_le := card_le_card -@[deprecated] alias card_lt_of_lt := card_lt_card +@[deprecated] alias card_le_of_le := card_le_card -- 2023-12-27 +@[deprecated] alias card_lt_of_lt := card_lt_card -- 2023-12-27 end Multiset diff --git a/Mathlib/Data/NNRat/Defs.lean b/Mathlib/Data/NNRat/Defs.lean index c195b123c510ba..47a88f3d0fd809 100644 --- a/Mathlib/Data/NNRat/Defs.lean +++ b/Mathlib/Data/NNRat/Defs.lean @@ -195,8 +195,7 @@ theorem mk_natCast (n : ℕ) : @Eq ℚ≥0 (⟨(n : ℚ), n.cast_nonneg⟩ : ℚ rfl #align nnrat.mk_coe_nat NNRat.mk_natCast --- 2024-04-05 -@[deprecated] alias mk_coe_nat := mk_natCast +@[deprecated] alias mk_coe_nat := mk_natCast -- 2024-04-05 @[simp] theorem coe_coeHom : ⇑coeHom = ((↑) : ℚ≥0 → ℚ) := diff --git a/Mathlib/Data/Nat/Digits.lean b/Mathlib/Data/Nat/Digits.lean index 24955b42cf7da6..8b9c8373430eba 100644 --- a/Mathlib/Data/Nat/Digits.lean +++ b/Mathlib/Data/Nat/Digits.lean @@ -752,8 +752,7 @@ lemma toDigitsCore_lens_eq_aux (b f : Nat) : specialize ih (n / b) (Nat.digitChar (n % b) :: l1) (Nat.digitChar (n % b) :: l2) simp only [List.length, congrArg (fun l ↦ l + 1) hlen] at ih exact ih trivial --- deprecated 2024-02-19 -@[deprecated] alias to_digits_core_lens_eq_aux:= toDigitsCore_lens_eq_aux +@[deprecated] alias to_digits_core_lens_eq_aux:= toDigitsCore_lens_eq_aux -- 2024-02-19 lemma toDigitsCore_lens_eq (b f : Nat) : ∀ (n : Nat) (c : Char) (tl : List Char), (Nat.toDigitsCore b f n (c :: tl)).length = (Nat.toDigitsCore b f n tl).length + 1 := by @@ -770,8 +769,7 @@ lemma toDigitsCore_lens_eq (b f : Nat) : ∀ (n : Nat) (c : Char) (tl : List Cha have lens_eq : (x :: (c :: tl)).length = (c :: x :: tl).length := by simp apply toDigitsCore_lens_eq_aux exact lens_eq --- deprecated 2024-02-19 -@[deprecated] alias to_digits_core_lens_eq:= toDigitsCore_lens_eq +@[deprecated] alias to_digits_core_lens_eq:= toDigitsCore_lens_eq -- 2024-02-19 lemma nat_repr_len_aux (n b e : Nat) (h_b_pos : 0 < b) : n < b ^ e.succ → n / b < b ^ e := by simp only [Nat.pow_succ] @@ -802,8 +800,7 @@ lemma toDigitsCore_length (b : Nat) (h : 2 <= b) (f n e : Nat) have _ : b ^ 1 = b := by simp only [Nat.pow_succ, pow_zero, Nat.one_mul] have _ : n < b := ‹b ^ 1 = b› ▸ hlt simp [(@Nat.div_eq_of_lt n b ‹n < b› : n / b = 0)] --- deprecated 2024-02-19 -@[deprecated] alias to_digits_core_length := toDigitsCore_length +@[deprecated] alias to_digits_core_length := toDigitsCore_length -- 2024-02-19 /-- The core implementation of `Nat.repr` returns a String with length less than or equal to the number of digits in the decimal number (represented by `e`). For example, the decimal string diff --git a/Mathlib/Data/Rat/Defs.lean b/Mathlib/Data/Rat/Defs.lean index 6019dd9ff88025..e7f084a2016dd4 100644 --- a/Mathlib/Data/Rat/Defs.lean +++ b/Mathlib/Data/Rat/Defs.lean @@ -194,13 +194,12 @@ lemma neg_def (q : ℚ) : -q = -q.num /. q.den := by rw [← neg_divInt, num_div @[simp] lemma divInt_neg (n d : ℤ) : n /. -d = -n /. d := divInt_neg' .. #align rat.mk_neg_denom Rat.divInt_neg --- 2024-03-18 -@[deprecated] alias divInt_neg_den := divInt_neg +@[deprecated] alias divInt_neg_den := divInt_neg -- 2024-03-18 attribute [simp] divInt_sub_divInt --- 2024-03-18 -@[deprecated divInt_sub_divInt] lemma sub_def'' {a b c d : ℤ} (b0 : b ≠ 0) (d0 : d ≠ 0) : +@[deprecated divInt_sub_divInt] -- 2024-03-18 +lemma sub_def'' {a b c d : ℤ} (b0 : b ≠ 0) (d0 : d ≠ 0) : a /. b - c /. d = (a * d - c * b) /. (b * d) := divInt_sub_divInt _ _ b0 d0 #align rat.sub_def Rat.sub_def'' @@ -270,8 +269,7 @@ protected theorem add_assoc : a + b + c = a + (b + c) := protected lemma add_left_neg : -a + a = 0 := by simp [add_def, normalize_eq_mkRat] #align rat.add_left_neg Rat.add_left_neg --- 2024-03-18 -@[deprecated zero_divInt] lemma divInt_zero_one : 0 /. 1 = 0 := zero_divInt _ +@[deprecated zero_divInt] lemma divInt_zero_one : 0 /. 1 = 0 := zero_divInt _ -- 2024-03-18 #align rat.mk_zero_one Rat.zero_divInt @[simp] lemma divInt_one (n : ℤ) : n /. 1 = n := by simp [divInt, mkRat, normalize] @@ -280,8 +278,8 @@ protected lemma add_left_neg : -a + a = 0 := by simp [add_def, normalize_eq_mkRa lemma divInt_one_one : 1 /. 1 = 1 := by rw [divInt_one]; rfl #align rat.mk_one_one Rat.divInt_one_one --- 2024-03-18 -@[deprecated divInt_one] lemma divInt_neg_one_one : -1 /. 1 = -1 := by rw [divInt_one]; rfl +@[deprecated divInt_one] -- 2024-03-18 +lemma divInt_neg_one_one : -1 /. 1 = -1 := by rw [divInt_one]; rfl #align rat.mk_neg_one_one Rat.divInt_neg_one_one #align rat.mul_one Rat.mul_one diff --git a/Mathlib/Data/Real/NNReal.lean b/Mathlib/Data/Real/NNReal.lean index 37e85a869e37c3..26fce771c3b022 100644 --- a/Mathlib/Data/Real/NNReal.lean +++ b/Mathlib/Data/Real/NNReal.lean @@ -401,8 +401,7 @@ theorem mk_natCast (n : ℕ) : @Eq ℝ≥0 (⟨(n : ℝ), n.cast_nonneg⟩ : ℝ NNReal.eq (NNReal.coe_natCast n).symm #align nnreal.mk_coe_nat NNReal.mk_natCast --- 2024-04-05 -@[deprecated] alias mk_coe_nat := mk_natCast +@[deprecated] alias mk_coe_nat := mk_natCast -- 2024-04-05 -- Porting note: place this in the `Real` namespace @[simp] diff --git a/Mathlib/Data/Subtype.lean b/Mathlib/Data/Subtype.lean index 8f4bc6085484d9..4f66514d45f416 100644 --- a/Mathlib/Data/Subtype.lean +++ b/Mathlib/Data/Subtype.lean @@ -141,8 +141,7 @@ theorem val_inj {a b : Subtype p} : a.val = b.val ↔ a = b := lemma coe_ne_coe {a b : Subtype p} : (a : α) ≠ b ↔ a ≠ b := coe_injective.ne_iff --- 2024-04-04 -@[deprecated] alias ⟨ne_of_val_ne, _⟩ := coe_ne_coe +@[deprecated] alias ⟨ne_of_val_ne, _⟩ := coe_ne_coe -- 2024-04-04 #align subtype.ne_of_val_ne Subtype.ne_of_val_ne -- Porting note: it is unclear why the linter doesn't like this. diff --git a/Mathlib/Data/ZMod/Quotient.lean b/Mathlib/Data/ZMod/Quotient.lean index e1781faa14467e..9ed81851103be6 100644 --- a/Mathlib/Data/ZMod/Quotient.lean +++ b/Mathlib/Data/ZMod/Quotient.lean @@ -153,8 +153,9 @@ theorem orbitZPowersEquiv_symm_apply (k : ZMod (minimalPeriod (a • ·) b)) : rfl #align mul_action.orbit_zpowers_equiv_symm_apply MulAction.orbitZPowersEquiv_symm_apply #align add_action.orbit_zmultiples_equiv_symm_apply AddAction.orbitZMultiplesEquiv_symm_apply -/- 2024-02-21 -/ @[deprecated] alias _root_.AddAction.orbit_zmultiples_equiv_symm_apply := - orbitZMultiplesEquiv_symm_apply + +@[deprecated] -- 2024-02-21 +alias _root_.AddAction.orbit_zmultiples_equiv_symm_apply := orbitZMultiplesEquiv_symm_apply theorem orbitZPowersEquiv_symm_apply' (k : ℤ) : (orbitZPowersEquiv a b).symm k = diff --git a/Mathlib/Deprecated/Submonoid.lean b/Mathlib/Deprecated/Submonoid.lean index 5d2442f6ff8419..00860c9d64fdf9 100644 --- a/Mathlib/Deprecated/Submonoid.lean +++ b/Mathlib/Deprecated/Submonoid.lean @@ -222,7 +222,7 @@ theorem IsSubmonoid.powers_subset {a : M} (hs : IsSubmonoid s) (h : a ∈ s) : p fun _ ⟨_, hx⟩ => hx ▸ hs.pow_mem h #align is_submonoid.power_subset IsSubmonoid.powers_subset #align is_add_submonoid.multiples_subset IsAddSubmonoid.multiples_subset -/- 2024-02-21 -/ @[deprecated] alias IsSubmonoid.power_subset := IsSubmonoid.powers_subset +@[deprecated] alias IsSubmonoid.power_subset := IsSubmonoid.powers_subset -- 2024-02-21 end powers diff --git a/Mathlib/FieldTheory/PrimitiveElement.lean b/Mathlib/FieldTheory/PrimitiveElement.lean index 3361e273c1a835..1e9c0f1ad16f69 100644 --- a/Mathlib/FieldTheory/PrimitiveElement.lean +++ b/Mathlib/FieldTheory/PrimitiveElement.lean @@ -290,7 +290,7 @@ theorem FiniteDimensional.of_finite_intermediateField rw [htop] at hfin exact topEquiv.toLinearEquiv.finiteDimensional -@[deprecated] -- Since 2024/02/02 +@[deprecated] -- Since 2024-02-02 alias finiteDimensional_of_finite_intermediateField := FiniteDimensional.of_finite_intermediateField theorem exists_primitive_element_of_finite_intermediateField @@ -311,7 +311,7 @@ theorem FiniteDimensional.of_exists_primitive_element (halg : Algebra.IsAlgebrai rw [hprim] at hfin exact topEquiv.toLinearEquiv.finiteDimensional -@[deprecated] -- Since 2024/02/02 +@[deprecated] -- Since 2024-02-02 alias finiteDimensional_of_exists_primitive_element := FiniteDimensional.of_exists_primitive_element -- A finite simple extension has only finitely many intermediate fields diff --git a/Mathlib/LinearAlgebra/FiniteDimensional.lean b/Mathlib/LinearAlgebra/FiniteDimensional.lean index 76217753cec47f..9987a6bb723f91 100644 --- a/Mathlib/LinearAlgebra/FiniteDimensional.lean +++ b/Mathlib/LinearAlgebra/FiniteDimensional.lean @@ -368,21 +368,21 @@ theorem FiniteDimensional.of_rank_eq_nat {n : ℕ} (h : Module.rank K V = n) : Module.finite_of_rank_eq_nat h #align finite_dimensional_of_rank_eq_nat FiniteDimensional.of_rank_eq_nat -@[deprecated] -- Since 2024/02/02 +@[deprecated] -- Since 2024-02-02 alias finiteDimensional_of_rank_eq_nat := FiniteDimensional.of_rank_eq_nat theorem FiniteDimensional.of_rank_eq_zero (h : Module.rank K V = 0) : FiniteDimensional K V := Module.finite_of_rank_eq_zero h #align finite_dimensional_of_rank_eq_zero FiniteDimensional.of_rank_eq_zero -@[deprecated] -- Since 2024/02/02 +@[deprecated] -- Since 2024-02-02 alias finiteDimensional_of_rank_eq_zero := FiniteDimensional.of_rank_eq_zero theorem FiniteDimensional.of_rank_eq_one (h : Module.rank K V = 1) : FiniteDimensional K V := Module.finite_of_rank_eq_one h #align finite_dimensional_of_rank_eq_one FiniteDimensional.of_rank_eq_one -@[deprecated] -- Since 2024/02/02 +@[deprecated] -- Since 2024-02-02 alias finiteDimensional_of_rank_eq_one := FiniteDimensional.of_rank_eq_one variable (K V) diff --git a/Mathlib/Logic/Function/Conjugate.lean b/Mathlib/Logic/Function/Conjugate.lean index 0f974e7321a838..0af5db2542b1e4 100644 --- a/Mathlib/Logic/Function/Conjugate.lean +++ b/Mathlib/Logic/Function/Conjugate.lean @@ -67,7 +67,7 @@ then `fbc ∘ fab` semiconjugates `ga` to `gc`. See also `Function.Semiconj.trans` for a version with reversed arguments. -**Backward compatibility note:** before 2024/01/13, +**Backward compatibility note:** before 2024-01-13, this lemma used to have the same order of arguments that `Function.Semiconj.trans` has now. -/ theorem comp_left (hbc : Semiconj fbc gb gc) (hab : Semiconj fab ga gb) : Semiconj (fbc ∘ fab) ga gc := diff --git a/Mathlib/MeasureTheory/Function/L1Space.lean b/Mathlib/MeasureTheory/Function/L1Space.lean index 271865d42596d5..3bc7a3cb9520a4 100644 --- a/Mathlib/MeasureTheory/Function/L1Space.lean +++ b/Mathlib/MeasureTheory/Function/L1Space.lean @@ -185,8 +185,7 @@ theorem HasFiniteIntegral.of_finite [Finite α] [IsFiniteMeasure μ] {f : α → let ⟨_⟩ := nonempty_fintype α hasFiniteIntegral_of_bounded <| ae_of_all μ <| norm_le_pi_norm f -@[deprecated] -- Since 2024/02/05 -alias hasFiniteIntegral_of_fintype := HasFiniteIntegral.of_finite +@[deprecated] alias hasFiniteIntegral_of_fintype := HasFiniteIntegral.of_finite -- Since 2024-02-05 theorem HasFiniteIntegral.mono_measure {f : α → β} (h : HasFiniteIntegral f ν) (hμ : μ ≤ ν) : HasFiniteIntegral f μ := @@ -500,8 +499,7 @@ theorem Integrable.of_finite [Finite α] [MeasurableSpace α] [MeasurableSinglet (μ : Measure α) [IsFiniteMeasure μ] (f : α → β) : Integrable (fun a ↦ f a) μ := ⟨(StronglyMeasurable.of_finite f).aestronglyMeasurable, .of_finite⟩ -@[deprecated] -- Since 2024/02/05 -alias integrable_of_fintype := Integrable.of_finite +@[deprecated] alias integrable_of_fintype := Integrable.of_finite -- Since 2024-02-05 theorem Memℒp.integrable_norm_rpow {f : α → β} {p : ℝ≥0∞} (hf : Memℒp f p μ) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞) : Integrable (fun x : α => ‖f x‖ ^ p.toReal) μ := by diff --git a/Mathlib/MeasureTheory/Function/SimpleFunc.lean b/Mathlib/MeasureTheory/Function/SimpleFunc.lean index 3a71fdc9c84ef8..90adad34e5575c 100644 --- a/Mathlib/MeasureTheory/Function/SimpleFunc.lean +++ b/Mathlib/MeasureTheory/Function/SimpleFunc.lean @@ -91,8 +91,7 @@ def ofFinite [Finite α] [MeasurableSingletonClass α] (f : α → β) : α → measurableSet_fiber' x := (toFinite (f ⁻¹' {x})).measurableSet finite_range' := Set.finite_range f -@[deprecated] -- Since 2024/02/05 -alias ofFintype := ofFinite +@[deprecated] alias ofFintype := ofFinite -- Since 2024-02-05 /-- Simple function defined on the empty type. -/ def ofIsEmpty [IsEmpty α] : α →ₛ β := ofFinite isEmptyElim diff --git a/Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean b/Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean index 2141e0330d9534..26b2dce43935fa 100644 --- a/Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean +++ b/Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean @@ -138,7 +138,7 @@ theorem StronglyMeasurable.of_finite [Finite α] {_ : MeasurableSpace α} (f : α → β) : StronglyMeasurable f := ⟨fun _ => SimpleFunc.ofFinite f, fun _ => tendsto_const_nhds⟩ -@[deprecated] -- Since 2024/02/05 +@[deprecated] -- Since 2024-02-05 alias stronglyMeasurable_of_fintype := StronglyMeasurable.of_finite @[deprecated StronglyMeasurable.of_finite] diff --git a/Mathlib/RingTheory/UniqueFactorizationDomain.lean b/Mathlib/RingTheory/UniqueFactorizationDomain.lean index ee7764ed128316..451fa17e589716 100644 --- a/Mathlib/RingTheory/UniqueFactorizationDomain.lean +++ b/Mathlib/RingTheory/UniqueFactorizationDomain.lean @@ -1462,7 +1462,7 @@ theorem factors_zero : (0 : Associates α).factors = ⊤ := dif_pos rfl #align associates.factors_0 Associates.factors_zero -@[deprecated] alias factors_0 := factors_zero -- 2024/03/16 +@[deprecated] alias factors_0 := factors_zero -- 2024-03-16 @[simp] theorem factors_mk (a : α) (h : a ≠ 0) : (Associates.mk a).factors = factors' a := by diff --git a/Mathlib/Topology/Bases.lean b/Mathlib/Topology/Bases.lean index a1bab3d5e4d4f9..880e9a02c9c567 100644 --- a/Mathlib/Topology/Bases.lean +++ b/Mathlib/Topology/Bases.lean @@ -553,14 +553,14 @@ theorem IsSeparable.of_subtype (s : Set α) [SeparableSpace s] : IsSeparable s : simpa using isSeparable_range (continuous_subtype_val (p := (· ∈ s))) #align topological_space.is_separable_of_separable_space_subtype TopologicalSpace.IsSeparable.of_subtype -@[deprecated] -- Since 2024/02/05 +@[deprecated] -- Since 2024-02-05 alias isSeparable_of_separableSpace_subtype := IsSeparable.of_subtype theorem IsSeparable.of_separableSpace [h : SeparableSpace α] (s : Set α) : IsSeparable s := IsSeparable.mono (isSeparable_univ_iff.2 h) (subset_univ _) #align topological_space.is_separable_of_separable_space TopologicalSpace.IsSeparable.of_separableSpace -@[deprecated] -- Since 2024/02/05 +@[deprecated] -- Since 2024-02-05 alias isSeparable_of_separableSpace := IsSeparable.of_separableSpace end TopologicalSpace diff --git a/Mathlib/Topology/CompactOpen.lean b/Mathlib/Topology/CompactOpen.lean index b0afca670053ca..51c699c589f281 100644 --- a/Mathlib/Topology/CompactOpen.lean +++ b/Mathlib/Topology/CompactOpen.lean @@ -150,7 +150,7 @@ lemma _root_.Continuous.compCM (hg : Continuous g) (hf : Continuous f) : Continuous fun x => (g x).comp (f x) := continuous_comp'.comp (hf.prod_mk hg) -@[deprecated _root_.Continuous.compCM] -- deprecated on 2024/01/30 +@[deprecated _root_.Continuous.compCM] -- deprecated on 2024-01-30 lemma continuous.comp' (hf : Continuous f) (hg : Continuous g) : Continuous fun x => (g x).comp (f x) := hg.compCM hf diff --git a/Mathlib/Topology/MetricSpace/ProperSpace.lean b/Mathlib/Topology/MetricSpace/ProperSpace.lean index cbf9b1a14d4091..70d387f4ba3d8e 100644 --- a/Mathlib/Topology/MetricSpace/ProperSpace.lean +++ b/Mathlib/Topology/MetricSpace/ProperSpace.lean @@ -68,7 +68,7 @@ theorem ProperSpace.of_isCompact_closedBall_of_le (R : ℝ) (closedBall_subset_closedBall <| le_max_left _ _)⟩ #align proper_space_of_compact_closed_ball_of_le ProperSpace.of_isCompact_closedBall_of_le -@[deprecated] -- Since 2024/01/31 +@[deprecated] -- Since 2024-01-31 alias properSpace_of_compact_closedBall_of_le := ProperSpace.of_isCompact_closedBall_of_le /-- If there exists a sequence of compact closed balls with the same center diff --git a/Mathlib/Topology/Order.lean b/Mathlib/Topology/Order.lean index dc4cad0dfa7af2..13b89f9a7027e4 100644 --- a/Mathlib/Topology/Order.lean +++ b/Mathlib/Topology/Order.lean @@ -611,7 +611,7 @@ theorem nhds_nhdsAdjoint_same (a : α) (f : Filter α) : exact IsOpen.mem_nhds (fun _ ↦ htf) hat · exact sup_le (pure_le_nhds _) ((gc_nhds a).le_u_l f) -@[deprecated] -- Since 2024/02/10 +@[deprecated] -- Since 2024-02-10 alias nhdsAdjoint_nhds := nhds_nhdsAdjoint_same #align nhds_adjoint_nhds nhdsAdjoint_nhds @@ -620,7 +620,7 @@ theorem nhds_nhdsAdjoint_of_ne {a b : α} (f : Filter α) (h : b ≠ a) : let _ := nhdsAdjoint a f (isOpen_singleton_iff_nhds_eq_pure _).1 <| isOpen_singleton_nhdsAdjoint f h -@[deprecated nhds_nhdsAdjoint_of_ne] -- Since 2024/02/10 +@[deprecated nhds_nhdsAdjoint_of_ne] -- Since 2024-02-10 theorem nhdsAdjoint_nhds_of_ne (a : α) (f : Filter α) {b : α} (h : b ≠ a) : @nhds α (nhdsAdjoint a f) b = pure b := nhds_nhdsAdjoint_of_ne f h