eval_apply_ofReal — Mathlib

English

The evaluation of cyclotomic n over ℂ at a real number q coincides with the evaluation of cyclotomic n over ℝ at q when viewed via the natural embedding ℝ → ℂ.

Русский

Значение циклотоми́ческого n в ℂ при q совпадает с значением циклотоми́ческого n в ℝ при q через естественное вложение ℝ → ℂ.

LaTeX

$$$\operatorname{eval}(\mathrm{algebraMap}\,\mathbb{R}\mathbb{C}\ q)(\operatorname{cyclotomic} n \mathbb{C}) = \operatorname{eval}(q, \operatorname{cyclotomic} n \mathbb{R})$$$

Lean4

@[simp]
theorem eval_apply_ofReal (q : ℝ) (n : ℕ) : eval (q : ℂ) (cyclotomic n ℂ) = (eval q (cyclotomic n ℝ)) :=
  cyclotomic.eval_apply q n (algebraMap ℝ ℂ)

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