coe_polynomial — Mathlib

English

The coercion of a polynomial map coincides with the polynomial map of the induced equivariant map.

Русский

Приведение отображения многочлена совпадает с отображением многочлена индуцированного эквиариантного отображения.

LaTeX

$$$$\text{coe polynomials}$$$$

Lean4

@[simp]
theorem coe_polynomial (g : P →+*[M] Q) : (g.polynomial : P[X] → Q[X]) = map g :=
  rfl

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