eval₂Hom_zero' — Mathlib

English

The evaluation homomorphism at a zero function on σ maps to the composition with constantCoeff: eval₂Hom f (0) = f ∘ constantCoeff.

Русский

Оценочное отображение по нулю: eval₂Hom f (0) = f ∘ constantCoeff.

LaTeX

$$$$ \mathrm{eval_2Hom} \; f \; (0 : σ \to S_2) = f \circ \text{constantCoeff} $$$$

Lean4

@[simp]
theorem eval₂Hom_zero' (f : R →+* S₂) : eval₂Hom f (fun _ => 0 : σ → S₂) = f.comp constantCoeff :=
  eval₂Hom_zero f

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