algebraMap_posRootForm_posForm — Mathlib

English

Algebra map sends RootFormIn to RootForm via a commutative diagram.

Русский

Алгебраическое отображение переводит RootFormIn в RootForm по диаграмме совместимости.

LaTeX

$$$(\\mathrm{algebraMap}\ S R)(P.RootFormIn S x y) = P.RootForm x y$$$

Lean4

theorem algebraMap_posRootForm_posForm (x y : span S (range P.root)) :
    (algebraMap S R) ((P.posRootForm S).posForm x y) = P.RootForm x y := by simp [posRootForm]

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