associated_rightInverse — Mathlib

English

associatedHom is a right inverse of toQuadraticMap, up to the BilinMap embedding.

Русский

associatedHom является правым обратным к toQuadraticMap в рамках вложения BilinMap.

LaTeX

$$$ \text{associated_rightInverse} : \; \text{associatedHom } S \; \rightarrow \; (\text{toQuadraticMap} )^{-1} $$$

Lean4

theorem associated_rightInverse :
    Function.RightInverse (associatedHom S) (BilinMap.toQuadraticMap : _ → QuadraticMap R M N) :=
  toQuadraticMap_associated S

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