algebraMap_leftInverse — Mathlib

English

Algebra map from R into FreeAlgebra R X has a left inverse provided by algebraMapInv.

Русский

О отображении алгебра от R в FreeAlgebra R X имеется левообратное, задаваемое algebraMapInv.

LaTeX

$$$\text{LeftInverse } algebraMapInv \ (algebraMap R \lvert FreeAlgebra R X)$$$

Lean4

theorem algebraMap_leftInverse : Function.LeftInverse algebraMapInv (algebraMap R <| FreeAlgebra R X) := fun x ↦ by
  simp [algebraMapInv]

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