mapRangeRingHom_apply — Mathlib

English

The mapRangeRingHom M f is a ring hom that on any element x ∈ R[M] evaluates to applying f coefficientwise: (mapRangeRingHom M f)(x) m = f(x m).

Русский

mapRangeRingHom M f — кольцевой гомоморфизм, который поэлементно применяет f к коэффициентам: (mapRangeRingHom M f)(x) m = f(x m).

LaTeX

$$$ (mapRangeRingHom\ M\ f)\; x\; m = f\left(x\left(m\right)\right) $$$

Lean4

@[simp]
theorem mapRangeRingHom_apply (f : R →+* S) (x : R[M]) (m : M) : mapRangeRingHom M f x m = f (x m) := by
  classical
  induction x using induction_linear
  · simp
  · simp [*]
  · simp [mapRangeRingHom, single_apply, apply_ite (f := f)]

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