comp_aeval_apply — Mathlib

English

For all p, φ(aeval_f p) equals aeval_{i ↦ φ(f(i))} applied to p.

Русский

Для любого p верно, что φ(aeval_f(p)) = aeval_{i ↦ φ(f(i))}(p).

LaTeX

$$$$ \phi \big( \mathrm{aeval}_f(p) \big) = \mathrm{aeval}_{\, (i \mapsto \phi(f(i)))}(p) $$$$

Lean4

theorem comp_aeval_apply {B : Type*} [CommSemiring B] [Algebra R B] (φ : S₁ →ₐ[R] B) (p : MvPolynomial σ R) :
    φ (aeval f p) = aeval (fun i ↦ φ (f i)) p := by rw [← comp_aeval, AlgHom.coe_comp, comp_apply]

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