int_eval₂_eq — Mathlib

English

For any x in L, eval₂ with the algebra map on P.int R hP equals aeval x applied to P.

Русский

Для любого x в L, eval₂ с алгебраическим отображением на P.int R hP равно aeval x(P).

LaTeX

$$$\mathrm{eval_2}(\mathrm{algebraMap}\_{R,L},x, P^{\mathrm{int}}_{R,hP}) = \mathrm{aeval}_x(P)$$$

Lean4

@[simp]
theorem int_eval₂_eq (x : L) : eval₂ (algebraMap R L) x (P.int R hP) = aeval x P :=
  by
  rw [aeval_eq_sum_range, eval₂_eq_sum_range]
  exact Finset.sum_congr rfl (fun n _ => by rw [Algebra.smul_def]; rfl)

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