smul_eq_map — Mathlib

English

The action of M on polynomials is realized by applying the corresponding ring homomorphism to coefficients, i.e., m • p = map (MulSemiringAction.toRingHom M R m) p.

Русский

Действие элемента M на многочленах реализуется через соответствующий кольцевой однородный гомоморфизм на коэффициентах: m • p = map (MulSemiringAction.toRingHom M R m) p.

LaTeX

$$$\forall m,\ (m \cdot p) = \operatorname{map}(\operatorname{MulSemiringAction.toRingHom M R m})\ p.$$$

Lean4

theorem smul_eq_map [MulSemiringAction M R] (m : M) : HSMul.hSMul m = map (MulSemiringAction.toRingHom M R m) :=
  by
  ext
  simp

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