complex_ofReal_eval_T — Mathlib

English

The real Chebyshev polynomial evaluates compatibly with its complex counterpart: evaluating T_R n at real x and then embedding in C equals evaluating T_C n at x viewed as complex.

Русский

Неравенство совместимо между вещественным и комплексным вариантами полинома Чебышева: значение T_R n при x ∈ ℝ равняется значению T_C n при x ∈ ℂ после естественного включения.

LaTeX

$$$(((T \mathbb{R} n).eval x : \mathbb{R}) : \mathbb{C}) = (T \mathbb{C} n).eval (x : \mathbb{C})$$$

Lean4

@[simp, norm_cast]
theorem complex_ofReal_eval_T : ∀ (x : ℝ) n, (((T ℝ n).eval x : ℝ) : ℂ) = (T ℂ n).eval (x : ℂ) :=
  @algebraMap_eval_T ℝ ℂ _ _ _

Похожие утверждения