Mathlib Map

Theorems · Theorem · special functions

Polynomial.Chebyshev.isExtrOn_T_real_iff

∀ {n : ℕ},
  n ≠ 0 →
    ∀ {x : ℝ},
      x ∈ Set.Icc (-1) 1 →
        (IsExtrOn (fun x => Polynomial.eval x (Polynomial.Chebyshev.T ℝ ↑n)) (Set.Icc (-1) 1) x ↔
          ∃ k ≤ n, x = Real.cos (↑k * Real.pi / ↑n))
Defined in
Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Cited by
0 results in Mathlib
Foundations
Depth 219 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Set · cited by 53352SetReal · cited by 25697Realone_mul · cited by 2841one_mulNat.cast_one · cited by 2501Nat.cast_oneReal.pi · cited by 1774Real.piSet.Icc · cited by 1702Set.IccMulZeroClass.zero_mul · cited by 1625MulZeroClass.zero_mulPolynomial.eval · cited by 796Polynomial.evalReal.cos · cited by 424Real.cosCharP.cast_eq_zero · cited by 357CharP.cast_eq_zerozero_div · cited by 222zero_divIsMaxOn · cited by 114IsMaxOnPolynomial.Chebyshev.T · cited by 108Chebyshev.TIsMinOn · cited by 96IsMinOnReal.cos_zero · cited by 38Real.cos_zeroChebyshev.isExtrOn_T_real_iffCITED BYCITES

Cites27

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.