constantCoeff_comp_map — Mathlib

English

As ring homomorphisms, composing the constant coefficient map with map f equals composing f with the constant coefficient map. In symbols, constantCoeff ∘ map_f = f ∘ constantCoeff.

Русский

При композиции отображения постоянного члена с map f получается то же, что и композиция f с отображением постоянного члена: constantCoeff ∘ map_f = f ∘ constantCoeff.

LaTeX

$$$$(\\\\text{constantCoeff} \\, \cdot \\, \mathrm{map}_f) = f \circ \text{constantCoeff}$$$$

Lean4

theorem constantCoeff_comp_map (f : R →+* S₁) :
    (constantCoeff : MvPolynomial σ S₁ →+* S₁).comp (MvPolynomial.map f) = f.comp constantCoeff := by ext <;> simp

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