eval₂Hom_zero — Mathlib

English

Same as the previous statement expressed with map_aeval, relating φ(aeval_g p) to eval₂Hom.

Русский

То же самое, что и предыдущее утверждение, выраженное через map_aeval, связывая φ(aeval_g p) с eval₂Hom.

LaTeX

$$$$ \phi( \mathrm{aeval}_g(p) ) = \mathrm{eval_2Hom}( \phi \circ \mathrm{algebraMap}, i \mapsto \phi(g(i)) )(p) $$$$

Lean4

@[simp]
theorem eval₂Hom_zero (f : R →+* S₂) : eval₂Hom f (0 : σ → S₂) = f.comp constantCoeff := by ext <;> simp

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