eval₂RingHom' — Mathlib

English

If p evaluates to zero, then the product p·q evaluates to zero as well.

Русский

Если p оценивается как ноль, то произведение p·q также оценивается как ноль.

LaTeX

$$$\text{If } \operatorname{ev}_{f,x}(p) = 0 \text{ then } (p q).\operatorname{ev}_{f,x} = 0$$$

Lean4

/-- `eval₂` as a `RingHom` for noncommutative rings -/
@[simps]
def eval₂RingHom' (f : R →+* S) (x : S) (hf : ∀ a, Commute (f a) x) : R[X] →+* S
    where
  toFun := eval₂ f x
  map_add' _ _ := eval₂_add _ _
  map_zero' := eval₂_zero _ _
  map_mul' _p q := eval₂_mul_noncomm f x fun k => hf <| coeff q k
  map_one' := eval₂_one _ _

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