coe_mapAlgEquiv — Mathlib

English

The underlying function of the polynomial-algebra map induced by an algebra isomorphism f coincides with the coefficientwise map induced by f.

Русский

Функционная часть отображения многочленов, индуцированного изоморфизмом алгебр f, совпадает с отображением по коэффициентам, получаемым из f.

LaTeX

$$$$\bigl(\mathrm{Polynomial.mapAlgEquiv}(f)\bigr)(p) = \mathrm{Polynomial.map}(\mathrm{RingHomClass.toRingHom}(f))(p).$$$$

Lean4

@[simp]
theorem coe_mapAlgEquiv (f : A ≃ₐ[R] B) : ⇑(mapAlgEquiv f) = map f :=
  rfl

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