posRootForm_eq — Mathlib

English

The posRootForm equals RootForm on spans, under injectivity of algebra map.

Русский

PosRootForm совпадает с RootForm на охватах при инъективности алгебраического отображения.

LaTeX

$$$P.posRootForm S = P.RootFormIn S$$$

Lean4

@[simp]
theorem posRootForm_eq : (P.posRootForm S).posForm = P.RootFormIn S :=
  by
  ext
  apply FaithfulSMul.algebraMap_injective S R
  simp only [algebraMap_posRootForm_posForm, algebraMap_rootFormIn]

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