aeval_conj — Mathlib

English

For a real-coefficient polynomial p and z in K, aeval(conj z) p equals conj(aeval z p).

Русский

Для многочлена p с вещественными коэффициентами и элемента z в K выполняется aeval(conn z) p = conj(aeval z p).

LaTeX

$$$\\mathrm{aeval}(\\overline{z})\,p = \\overline{\\mathrm{aeval}(z)\,p}$$$

Lean4

theorem aeval_conj (p : ℝ[X]) (z : K) : aeval (conj z) p = conj (aeval z p) :=
  aeval_algHom_apply (RCLike.conjAe (K := K)) z p

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