mapAlg_comp — Mathlib

English

A more general form of the same composition property for polynomials with multiple Algebras and IsScalarTower relations; composition of mapAlg maps is again mapAlg of the composed morphism.

Русский

Более общая форма свойства композиции для отображений mapAlg между несколькими алгебрами; композиция mapAlg равно mapAlg от составного морфизма.

LaTeX

$$$$ \forall p:\ Polynomial A,\ (\mathrm{mapAlg}\ A C) p = (\mathrm{mapAlg}\ B C)(\mathrm{mapAlg}\ A B p). $$$$

Lean4

theorem mapAlg_comp (p : A[X]) : (mapAlg A C) p = (mapAlg B C) (mapAlg A B p) := by
  simp [mapAlg_eq_map, map_map, IsScalarTower.algebraMap_eq A B C]

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