eval₂Hom — Mathlib

English

For the evaluation homomorphism, evaluating a constant C(r) yields f(r).

Русский

Для отображения оценки.eval₂Hom при константе C(r) получаем f(r).

LaTeX

$$$\operatorname{eval}_2^{Hom}(f,g)(C r) = f r$$$

Lean4

/-- `MvPolynomial.eval₂` as a `RingHom`. -/
def eval₂Hom (f : R →+* S₁) (g : σ → S₁) : MvPolynomial σ R →+* S₁
    where
  toFun := eval₂ f g
  map_one' := eval₂_one _ _
  map_mul' _ _ := eval₂_mul _ _
  map_zero' := eval₂_zero f g
  map_add' _ _ := eval₂_add _ _

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