Remove forwarding wrapper theorems with no callers

RealRooted/ASWKarlinSineBounds.lean

@@ -585,11 +585,4 @@ lemma signVariations_aswKarlinSineVector_degree_one_lt
     hle.trans (by lia)
   exact Nat.lt_of_le_pred horder hle'
 
-/-- Threshold-shaped wrapper for the degree-one sine upper bound. -/
-lemma signVariations_aswKarlinSineVector_degree_one_lt_of_lt_threshold
-    {θ : ℝ} {order : ℕ} (horder : 0 < order) (_hθ0 : 0 ≤ θ)
-    (_hθ : θ < aswSectorThreshold 1 order) :
-    Fin.signVariations (aswKarlinSineVector θ 1 order 1) < order :=
-  signVariations_aswKarlinSineVector_degree_one_lt θ horder
-
 end RealRooted

RealRooted/AffineFamily.lean

@@ -833,28 +833,6 @@ theorem allComboRealRooted_of_affine_family_nonneg
   allComboRealRooted_of_strictInterl
     (strictInterl_of_affine_family_nonneg hf0 hg0 hfnn hgnn haff)
 
-/-- Public shifted-pair package extracted from a nonnegative affine family.
-This is the corrected same-degree seam after the failed boundary-right-pair
-target: the affine family automatically promotes the shifted pair
-`(g + X * f, f)` into the clean succ-degree positive-combination regime. -/
-theorem shifted_pair_data_of_affine_family_nonneg
-    {f g : ℝ[X]}
-    (hf0 : f ≠ 0) (hg0 : g ≠ 0)
-    (hfnn : HasNonnegCoeffs f)
-    (hgnn : HasNonnegCoeffs g)
-    (haff :
-      ∀ {s t : ℝ}, 0 < s → 0 < t →
-        ((((C s * X + C t) * f) + g) ≠ 0 ∧ (((C s * X + C t) * f) + g).Splits)) :
-    PosComboRealRooted (g + X * f) f ∧
-    HasNonnegCoeffs (g + X * f) ∧
-    HasNonnegCoeffs f ∧
-    (g + X * f) ≠ 0 ∧
-    f ≠ 0 ∧
-    HasPosLeadingCoeff (g + X * f) ∧
-    HasPosLeadingCoeff f ∧
-    (g + X * f).natDegree = f.natDegree + 1 :=
-  affine_family_shifted_pair_data hf0 hg0 hfnn hgnn haff
-
 /-- A nonnegative affine family already orients the shifted pair:
 `f ≺ g + X * f`. This is the public corrected replacement for the earlier
 false attempt to orient every boundary pair `(C t * f + g, X * f)`. -/
@@ -894,21 +872,6 @@ theorem strictInterl_right_pair_of_affine_family_nonneg_sameDegree
     (strictInterl_shifted_pair_of_affine_family_nonneg hf0 hfnn hgnn haff)
     hf0 hg0 hfnn hgnn hdeg
 
-/-- Public shifted-pair reduction in the same-degree nonnegative regime:
-once the corrected shifted pair satisfies `f ≺ g + X * f`, the original pair
-already satisfies `f ≺ g`. This packages the internal subtraction step used in
-the affine-family same-degree branch. -/
-theorem strictInterl_of_strictInterl_shifted_pair_sameDegree_nonneg
-    {f g : ℝ[X]}
-    (h : StrictInterl f (g + X * f))
-    (hf0 : f ≠ 0) (hg0 : g ≠ 0)
-    (hfnn : HasNonnegCoeffs f)
-    (hgnn : HasNonnegCoeffs g)
-    (hdeg : g.natDegree = f.natDegree) :
-    StrictInterl f g :=
-  strictInterl_of_strictInterl_shifted_pair_sameDegree
-    h hf0 hg0 hfnn hgnn hdeg
-
 /-- Symmetric degree closeness for positive-combination real-rooted pairs with
 nonnegative coefficients. -/
 theorem natDegree_close_of_posComboRealRooted_of_nonnegCoeffs

RealRooted/BorceaBranden/Applications/AffineFiniteSymbol.lean

@@ -17,29 +17,13 @@ namespace RealRooted
 
 namespace BorceaBranden
 
-/-- Compatibility name for `complexificationLinearMap`. -/
-noncomputable abbrev complexifyLinearMap
-    (T : ℝ[X] →ₗ[ℝ] ℝ[X]) : ℂ[X] →ₗ[ℂ] ℂ[X] :=
-  complexificationLinearMap T
-
-@[simp] lemma complexifyLinearMap_monomial
-    (T : ℝ[X] →ₗ[ℝ] ℝ[X]) (n : ℕ) (z : ℂ) :
-    complexifyLinearMap T (Polynomial.monomial n z) =
-      C z * complexify (T (X ^ n)) :=
-  complexificationLinearMap_monomial T n z
-
-@[simp] lemma complexifyLinearMap_X_pow
+@[simp] lemma complexificationLinearMap_X_pow
     (T : ℝ[X] →ₗ[ℝ] ℝ[X]) (n : ℕ) :
-    complexifyLinearMap T ((X : ℂ[X]) ^ n) =
+    complexificationLinearMap T ((X : ℂ[X]) ^ n) =
       complexify (T ((X : ℝ[X]) ^ n)) := by
-  rw [Polynomial.X_pow_eq_monomial, complexifyLinearMap_monomial]
+  rw [Polynomial.X_pow_eq_monomial, complexificationLinearMap_monomial]
   simp
 
-lemma complexifyLinearMap_complexify
-    (T : ℝ[X] →ₗ[ℝ] ℝ[X]) (p : ℝ[X]) :
-    complexifyLinearMap T (complexify p) = complexify (T p) :=
-  complexificationLinearMap_complexify T p
-
 /-- The complex degree-box bidiagonal operator is the complexification of the
 real bidiagonal operator on a degree-bounded real input. -/
 lemma complexBidiagonalDegreeBox_value

RealRooted/CombinatorialExamples/SturmDerangementsExc.lean

@@ -573,31 +573,4 @@ theorem isSturmSeq_sturmDerangementsExcPrefix :
           simpa [sturmDerangementsExcPrefix, IsSturmSeq] using
             And.intro (interlaces_sturmDerangementsExc_succ (n := n + 2) (by lia)) ih
 
-/-- Backward-compatible alias while the project transitions away from the old name. -/
-abbrev warmupP := sturmDerangementsExc
-
-@[simp] lemma warmupP_zero : warmupP 0 = 0 := sturmDerangementsExc_zero
-
-@[simp] lemma warmupP_one : warmupP 1 = 0 := sturmDerangementsExc_one
-
-@[simp] lemma warmupP_two : warmupP 2 = X := sturmDerangementsExc_two
-
-lemma warmupP_recurrence (n : Nat) : warmupP (n + 3) =
-    X * (((n + 2 : ℝ[X])) * warmupP (n + 1) +
-      ((n + 2 : ℝ[X])) * warmupP (n + 2) +
-      (1 - X) * (warmupP (n + 2)).derivative) :=
-  sturmDerangementsExc_recurrence n
-
-lemma X_dvd_warmupP (n : Nat) : X ∣ warmupP n :=
-  X_dvd_sturmDerangementsExc n
-
-lemma warmupP_isRoot_zero (n : Nat) : (warmupP n).IsRoot 0 :=
-  sturmDerangementsExc_isRoot_zero n
-
-lemma warmupP_three : warmupP 3 = X ^ 2 + X := sturmDerangementsExc_three
-
-lemma warmupP_four : warmupP 4 = X ^ 3 + 7 * X ^ 2 + X := sturmDerangementsExc_four
-
-lemma warmupP_five : warmupP 5 = X ^ 4 + 21 * X ^ 3 + 21 * X ^ 2 + X := sturmDerangementsExc_five
-
 end RealRooted

RealRooted/CommonInterleaverSeq.lean

@@ -722,30 +722,6 @@ theorem pairHasCommonLeftInterleaver_symm {f g : ℝ[X]}
   obtain ⟨w, hf, hg⟩ := h
   exact ⟨w, hg, hf⟩
 
-/-- Extract the pair existential from `HasCommonInterleaver [f, g]`. -/
-theorem pairHasCommonInterleaver_of_hasCommonInterleaver_pair {f g : ℝ[X]}
-    (h : HasCommonInterleaver [f, g]) :
-    ∃ h : ℝ[X], StrictInterl f h ∧ StrictInterl g h :=
-  hasCommonInterleaver_pair.1 h
-
-/-- Package the pair existential as `HasCommonInterleaver [f, g]`. -/
-theorem hasCommonInterleaver_pair_of_pairHasCommonInterleaver {f g : ℝ[X]}
-    (h : ∃ h : ℝ[X], StrictInterl f h ∧ StrictInterl g h) :
-    HasCommonInterleaver [f, g] :=
-  hasCommonInterleaver_pair.2 h
-
-/-- Extract the left pair existential from `HasCommonLeftInterleaver [f, g]`. -/
-theorem pairHasCommonLeftInterleaver_of_hasCommonLeftInterleaver_pair
-    {f g : ℝ[X]} (h : HasCommonLeftInterleaver [f, g]) :
-    ∃ h : ℝ[X], StrictInterl h f ∧ StrictInterl h g :=
-  hasCommonLeftInterleaver_pair.1 h
-
-/-- Package the left pair existential as `HasCommonLeftInterleaver [f, g]`. -/
-theorem hasCommonLeftInterleaver_pair_of_pairHasCommonLeftInterleaver
-    {f g : ℝ[X]} (h : ∃ h : ℝ[X], StrictInterl h f ∧ StrictInterl h g) :
-    HasCommonLeftInterleaver [f, g] :=
-  hasCommonLeftInterleaver_pair.2 h
-
 /-- Extract the pair existential from `PairwiseHasCommonInterleaver [f, g]`. -/
 theorem pairHasCommonInterleaver_of_pairwiseHasCommonInterleaver_pair
     {f g : ℝ[X]} (h : PairwiseHasCommonInterleaver [f, g]) :

RealRooted/Compatibility/NDCutInvariant.lean

@@ -67,12 +67,6 @@ structure OrderedNDCutCompatible {m : ℕ}
 
 namespace OrderedNDCutCompatible
 
-/-- Receiver-style projection to the generic P/Q cut package. -/
-theorem toOrderedCutCompatible {m : ℕ} {N D : Fin m → ℝ[X]}
-    (h : OrderedNDCutCompatible N D) :
-    OrderedCutCompatible (ndCutP N D) (ndCutQ N D) :=
-  h.cutCompatible
-
 /-- Every `N` coordinate has nonnegative coefficients. -/
 theorem n_nonneg {m : ℕ} {N D : Fin m → ℝ[X]}
     (h : OrderedNDCutCompatible N D) (i : Fin m) :

RealRooted/Hadamard/Newton.lean

@@ -287,34 +287,6 @@ theorem normalized_coeff_nonneg_of_isPF (n : ℕ) {f : ℝ[X]}
     div_nonneg (hf.hasNonnegCoeffs k)
       (by exact_mod_cast Nat.zero_le (Nat.choose n k))
 
-/-- Constant normalized coefficient nonnegativity for a PF polynomial at
-binomial level three. -/
-theorem normalized_coeff_zero_nonneg_of_isPF_three {f : ℝ[X]}
-    (hf : IsPFPolynomial f) :
-    0 ≤ f.coeff 0 / (Nat.choose 3 0 : ℝ) :=
-  normalized_coeff_nonneg_of_isPF 3 hf 0
-
-/-- Linear normalized coefficient nonnegativity for a PF polynomial at
-binomial level three. -/
-theorem normalized_coeff_one_nonneg_of_isPF_three {f : ℝ[X]}
-    (hf : IsPFPolynomial f) :
-    0 ≤ f.coeff 1 / (Nat.choose 3 1 : ℝ) :=
-  normalized_coeff_nonneg_of_isPF 3 hf 1
-
-/-- Quadratic normalized coefficient nonnegativity for a PF polynomial at
-binomial level three. -/
-theorem normalized_coeff_two_nonneg_of_isPF_three {f : ℝ[X]}
-    (hf : IsPFPolynomial f) :
-    0 ≤ f.coeff 2 / (Nat.choose 3 2 : ℝ) :=
-  normalized_coeff_nonneg_of_isPF 3 hf 2
-
-/-- Cubic normalized coefficient nonnegativity for a PF polynomial at binomial
-level three. -/
-theorem normalized_coeff_three_nonneg_of_isPF_three {f : ℝ[X]}
-    (hf : IsPFPolynomial f) :
-    0 ≤ f.coeff 3 / (Nat.choose 3 3 : ℝ) :=
-  normalized_coeff_nonneg_of_isPF 3 hf 3
-
 /-- Normalized coefficient log-concavity of a degree-`≤ 3` PF polynomial.
 
 Writing `γ k = f.coeff k / (3.choose k)`, the adjacent cubic log-concavity

RealRooted/Interlacing/Residue.lean

@@ -18,24 +18,6 @@ namespace RealRooted
 
 /-! ## Derivative and evaluation signs -/
 
-theorem eval_derivative_eq_sum_real {p : ℝ[X]} (hp : p.Splits) (x : ℝ) :
-    p.derivative.eval x
-      = p.leadingCoeff *
-          (p.roots.map (fun r : ℝ =>
-            ((p.roots.erase r).map (fun s : ℝ => x - s)).prod)).sum :=
-  hp.eval_derivative x
-
-theorem deriv_sum_collapse (M : Multiset ℝ) (s : ℝ) (hs : s ∈ M) (hcount : M.count s = 1) :
-    (M.map (fun r : ℝ => ((M.erase r).map (fun t : ℝ => s - t)).prod)).sum
-      = ((M.erase s).map (fun t : ℝ => s - t)).prod :=
-  derivative_sum_collapse M s hs hcount
-
-theorem eval_derivative_at_root {p : ℝ[X]} (hp : p.Splits) (s : ℝ)
-    (hs : s ∈ p.roots) (hcount : p.roots.count s = 1) :
-    p.derivative.eval s
-      = p.leadingCoeff * ((p.roots.erase s).map (fun r : ℝ => s - r)).prod :=
-  hp.eval_derivative_at_root_of_roots_count_one s hs hcount
-
 theorem prod_sub_sign_pos (M : Multiset ℝ) (s : ℝ) (hs : s ∉ M) :
     0 < (M.map (fun r => s - r)).prod * (-1 : ℝ) ^ (M.countP (fun r => s < r)) := by
   induction M using Multiset.induction with

RealRooted/InterlacingSequenceBasic.lean

@@ -282,11 +282,6 @@ def IsInterlacingSeq0NonnegRealRooted (fs : List ℝ[X]) : Prop :=
 
 namespace IsInterlacingSeq0NonnegRealRooted
 
-lemma interlacingSeq0Nonneg {fs : List ℝ[X]}
-    (hfs : IsInterlacingSeq0NonnegRealRooted fs) :
-    IsInterlacingSeq0Nonneg fs :=
-  hfs.1
-
 lemma interlacingSeq0 {fs : List ℝ[X]}
     (hfs : IsInterlacingSeq0NonnegRealRooted fs) :
     IsInterlacingSeq0 fs :=

RealRooted/LiuWang/Step.lean

@@ -285,37 +285,6 @@ theorem strictInterl_lw_positive_C_mul_X_mul_lag_of_nonneg_coeffs
     (roots_nonpos_of_interlaces_of_nonneg_coeffs hgf hf_nonneg)
     hc hq_nonneg hF_pos hdeg_lo hdeg_hi hno
 
-/-- Family E `t R(t)` Liu--Wang step with an explicit half-line root
-certificate.  This is a named alias for the existing `X * q` product-lag
-wrapper, using `q` as the factor `R`. -/
-theorem strictInterl_lw_tR_lag_of_roots_nonpos {f g a R : ℝ[X]}
-    (hgf : Interlaces g f)
-    (hg_pos : HasPosLeadingCoeff g)
-    (hf_roots : ∀ r, f.IsRoot r → r ≤ 0)
-    (hR_nonneg : ∀ r, f.IsRoot r → 0 ≤ R.eval r)
-    (hF_pos : HasPosLeadingCoeff (a * f + (X * R) * g))
-    (hdeg_lo : f.natDegree ≤ (a * f + (X * R) * g).natDegree)
-    (hdeg_hi : (a * f + (X * R) * g).natDegree ≤ f.natDegree + 1)
-    (hno : ∀ r, f.IsRoot r → ¬ g.IsRoot r) :
-    StrictInterl f (a * f + (X * R) * g) :=
-  strictInterl_lw_positive_X_mul_lag_of_roots_nonpos
-    hgf hg_pos hf_roots hR_nonneg hF_pos hdeg_lo hdeg_hi hno
-
-/-- Family E `t R(t)` Liu--Wang step, deriving the half-line root bound from
-nonnegative coefficients of the current row. -/
-theorem strictInterl_lw_tR_lag_of_nonneg_coeffs {f g a R : ℝ[X]}
-    (hgf : Interlaces g f)
-    (hg_pos : HasPosLeadingCoeff g)
-    (hf_nonneg : HasNonnegCoeffs f)
-    (hR_nonneg : ∀ r, f.IsRoot r → 0 ≤ R.eval r)
-    (hF_pos : HasPosLeadingCoeff (a * f + (X * R) * g))
-    (hdeg_lo : f.natDegree ≤ (a * f + (X * R) * g).natDegree)
-    (hdeg_hi : (a * f + (X * R) * g).natDegree ≤ f.natDegree + 1)
-    (hno : ∀ r, f.IsRoot r → ¬ g.IsRoot r) :
-    StrictInterl f (a * f + (X * R) * g) :=
-  strictInterl_lw_positive_X_mul_lag_of_nonneg_coeffs
-    hgf hg_pos hf_nonneg hR_nonneg hF_pos hdeg_lo hdeg_hi hno
-
 /-- Family E `t(1-t)` Liu--Wang step with an explicit half-line root
 certificate. -/
 theorem strictInterl_lw_X_mul_one_sub_X_lag_of_roots_nonpos {f g a : ℝ[X]}

RealRooted/Mathlib/LinearAlgebra/Matrix/PerronFrobenius/Auxiliary.lean

@@ -328,10 +328,6 @@ lemma lt_not_le {α : Type*} [PartialOrder α] (x y : α) : x < y → ¬ (x ≥
 section ConditionallyCompleteLinearOrder
 
 variable {α : Type*} [ConditionallyCompleteLinearOrder α]
-/-- If y is an upper bound of a set s, and x is in s, then x ≤ y -/
-lemma le_of_mem_upperBounds {s : Set α} {x : α} {y : α} (hy : y ∈ upperBounds s) (hx : x ∈ s) :
-    x ≤ y := by
-  exact hy hx
 
 lemma bddAbove_iff_exists_upperBound {s : Set α} : BddAbove s ↔ ∃ b, ∀ x ∈ s, x ≤ b := by exact
   bddAbove_def

RealRooted/Mathlib/LinearAlgebra/Matrix/PerronFrobenius/CStarClasses.lean

@@ -28,9 +28,6 @@ theorem sq_eq_zero {R : Type*} [MonoidWithZero R] [NoZeroDivisors R] {x : R} :
   rw [pow_two, mul_eq_zero]
   exact or_self_iff
 
-/-- An element of a nonempty set. -/
-lemma Set.mem_of_nonempty {α : Type*} (s : Set α) (h : s.Nonempty) : ∃ x, x ∈ s := h
-
 /--
 An equality between real numbers implies an equality between their complex embeddings.
 -/

RealRooted/MultiplierSequence.lean

@@ -790,33 +790,6 @@ def finitePolyaSchurNonnegBackwardStatement : Prop :=
       IsPFPolynomial (jensenPolynomial n gamma) →
         IsFiniteMultiplierSequence n gamma
 
-/-- Low-degree base case of the backward finite Pólya--Schur direction.
-
-For `n ≤ 1`, the Jensen-polynomial hypothesis is unnecessary: diagonal
-operators preserve real-rootedness up to degree one for purely degree reasons. -/
-theorem finitePolyaSchurNonnegBackward_of_natDegree_le_one
-    {n : ℕ} (hn : n ≤ 1) {gamma : ℕ → ℝ}
-    (_hgamma : ∀ k, 0 ≤ gamma k)
-    (_hjensen : IsPFPolynomial (jensenPolynomial n gamma)) :
-    IsFiniteMultiplierSequence n gamma :=
-  isFiniteMultiplierSequence_of_natDegree_le_one hn gamma
-
-/-- Degree-zero case of the backward finite Pólya--Schur direction. -/
-theorem finitePolyaSchurNonnegBackward_natDegree_zero
-    {gamma : ℕ → ℝ}
-    (_hgamma : ∀ k, 0 ≤ gamma k)
-    (_hjensen : IsPFPolynomial (jensenPolynomial 0 gamma)) :
-    IsFiniteMultiplierSequence 0 gamma :=
-  isFiniteMultiplierSequence_natDegree_zero gamma
-
-/-- Degree-one case of the backward finite Pólya--Schur direction. -/
-theorem finitePolyaSchurNonnegBackward_natDegree_one
-    {gamma : ℕ → ℝ}
-    (_hgamma : ∀ k, 0 ≤ gamma k)
-    (_hjensen : IsPFPolynomial (jensenPolynomial 1 gamma)) :
-    IsFiniteMultiplierSequence 1 gamma :=
-  isFiniteMultiplierSequence_natDegree_one gamma
-
 /-- Degree at most two case of the backward finite Pólya--Schur direction. -/
 theorem finitePolyaSchurNonnegBackward_of_natDegree_le_two
     {n : ℕ} (hn : n ≤ 2) {gamma : ℕ → ℝ}

RealRooted/SameDegreeDerivative.lean

@@ -138,13 +138,6 @@ theorem roots_derivative_mem_Ioi_of_roots_mem_Ioi {p : ℝ[X]} {u : ℝ}
     ∀ r ∈ p.derivative.roots, r ∈ Set.Ioi u :=
   lt_roots_derivative_of_lt_roots hp hdeg h
 
-/-- Derivative root left-ray preservation. -/
-theorem roots_derivative_mem_Iio_of_roots_mem_Iio {p : ℝ[X]} {v : ℝ}
-    (hp : p.Splits) (hdeg : 2 ≤ p.natDegree)
-    (h : ∀ r ∈ p.roots, r ∈ Set.Iio v) :
-    ∀ r ∈ p.derivative.roots, r ∈ Set.Iio v :=
-  roots_derivative_lt_of_roots_lt hp hdeg h
-
 /-- Derivative root closed lower-ray preservation. -/
 theorem roots_derivative_mem_Ici_of_roots_mem_Ici {p : ℝ[X]} {u : ℝ}
     (hp : p.Splits) (hdeg : 2 ≤ p.natDegree)

RealRooted/ShiftLemma.lean

@@ -187,17 +187,4 @@ theorem strictInterl_shift
         hss_eq, hrs_eq, Or.inr ⟨hsamedeg, halt⟩⟩
       hdeg hf_pos hh_pos hf_nonpos hh_nonpos heval
 
-/-- Shift lemma with variables named for applications. -/
-theorem strictInterl_shift' {F H : ℝ[X]}
-    (hF_ne : F ≠ 0) (hF_splits : F.Splits) (hH_ne : H ≠ 0) (hH_splits : H.Splits)
-    (hF_nonpos : ∀ r ∈ F.roots, r ≤ 0)
-    (hH_nonpos : ∀ r ∈ H.roots, r ≤ 0)
-    (hF_pos : HasPosLeadingCoeff F)
-    (hH_pos : HasPosLeadingCoeff H)
-    (hstrictInterl : StrictInterl H F)
-    (heval : H.eval 0 ≤ F.eval 0) :
-    StrictInterl F (F + (X - C 1) * H) :=
-  strictInterl_shift hF_ne hF_splits hH_ne hH_splits hF_nonpos hH_nonpos hF_pos hH_pos
-    hstrictInterl heval
-
 end RealRooted

RealRooted/SuccDegreeLeftEndpoint.lean

@@ -370,16 +370,6 @@ theorem splits_of_closedSegment_family_of_succDegree
   rw [hEq] at hscaled
   exact hscaled
 
-/-- Right-family form of the succ-degree endpoint theorem. -/
-theorem splits_right_of_add_C_mul_family_of_succDegree
-    {f g : ℝ[X]}
-    (hfamily : ∀ {μ : ℝ}, 0 < μ → ((g + C μ * f) ≠ 0 ∧ (g + C μ * f).Splits))
-    (hf_pos : 0 < f.leadingCoeff)
-    (hg_pos : 0 < g.leadingCoeff)
-    (hsucc : f.natDegree = g.natDegree + 1) :
-    g.Splits :=
-  splits_of_add_C_mul_family_of_succDegree hfamily hg_pos hf_pos hsucc
-
 /-- Succ-degree positive-combination families split at the lower-degree
 endpoint. -/
 theorem PosComboRealRooted.left_splits_of_succDegree {f g : ℝ[X]}

RealRooted/Tactic/PFBidiagonal.lean

@@ -26,12 +26,6 @@ theorem splits_of_isPFPolynomial {p : ℝ[X]} (hp : IsPFPolynomial p) :
     p.Splits :=
   RealRooted.Tactic.pf_splits hp
 
-/-- Project one row from a PF sequence certificate. -/
-theorem at_of_isPFPolynomial_sequence {P : Nat → ℝ[X]}
-    (hP : ∀ n : Nat, IsPFPolynomial (P n)) (n : Nat) :
-    IsPFPolynomial (P n) :=
-  hP n
-
 /-- Project row-wise coefficient nonnegativity from a PF sequence certificate. -/
 theorem hasNonnegCoeffs_of_isPFPolynomial_sequence {P : Nat → ℝ[X]}
     (hP : ∀ n : Nat, IsPFPolynomial (P n)) :