coe_mapAlgHom — Mathlib

English

The underlying function of Polynomial.mapAlgHom f equals the map induced by f on coefficients: for any f : A →ₐ[R] B, (Polynomial.mapAlgHom f) = map f.

Русский

Базовая функция Polynomial.mapAlgHom f совпадает с отображением по коэффициентам, задаваемым функцией f: (Polynomial.mapAlgHom f) = map f.

LaTeX

$$⇑(Polynomial.mapAlgHom f) = map f$$

Lean4

@[simp]
theorem coe_mapAlgHom (f : A →ₐ[R] B) : ⇑(mapAlgHom f) = map f :=
  rfl

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