map_comp_C — Mathlib

English

Let f be a ring homomorphism. Then applying map to constants is the same as embedding the image of the constants through f.

Русский

Пусть f — гомоморфизм кольца. Тогда применение map к константам равно внедрению образа констант через f.

LaTeX

$$$$ (\mathrm{map}\, f) \circ MvPolynomial.C = MvPolynomial.C \circ f $$$$

Lean4

@[simp]
theorem map_comp_C (f : R →+* S) : (map f).comp (C : R →+* MvPolynomial σ R) = C.comp f :=
  by
  ext1
  apply map_C

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