algebraMap_leftInverse — Mathlib

English

The left inverse of ιInv is the map ι_R, i.e., composing ιInv with ι_R yields the identity on M.

Русский

Левая обратная к отображению ιInv является отображение ι_R, то есть ιInv ∘ ι_R = id_M.

LaTeX

$$$\\iota_R : M \\to \\mathrm{TensorAlgebra}_R(M),\\quad \\iotaInv \\circ \\iota_R = \\mathrm{id}_M$$$

Lean4

theorem algebraMap_leftInverse : Function.LeftInverse algebraMapInv (algebraMap R <| TensorAlgebra R M) := fun x => by
  simp [algebraMapInv]

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