complex_ofReal_eval_S — Mathlib

English

The real S polynomial evaluated at a real input matches the complex version under the natural embedding.

Русский

Соответствие для полиномов S при переходе в комплексные числа.

LaTeX

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

Lean4

@[simp, norm_cast]
theorem complex_ofReal_eval_S : ∀ (x : ℝ) n, (((S ℝ n).eval x : ℝ) : ℂ) = (S ℂ n).eval (x : ℂ) :=
  @algebraMap_eval_S ℝ ℂ _ _ _

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