aeval_pi — Mathlib

English

For an algebra homomorphism f, aeval (f x) = f ∘ aeval x.

Русский

Для алгебраического гомоморфизма f выполняется aeval (f x) = f ∘ aeval x.

LaTeX

$$$\forall f: A \to_{R} B,\; \operatorname{aeval}(f(x)) = f \circ \operatorname{aeval}(x).$$$

Lean4

/-- Polynomial evaluation on an indexed tuple is the indexed product of the evaluations
on the components.
Generalizes `Polynomial.aeval_prod` to indexed products. -/
theorem aeval_pi (x : Π i, A i) : aeval (R := R) x = Pi.algHom R A (fun i ↦ aeval (x i)) :=
  (funext fun i ↦ aeval_algHom (Pi.evalAlgHom R A i) x) ▸ (Pi.algHom_comp R A (Pi.evalAlgHom R A) (aeval x))

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