algebraMap_leftInverse — Mathlib

English

The map algebraMapInv is a left inverse of algebraMap R (ExteriorAlgebra R M); that is, algebraMapInv ∘ algebraMap = id_R.

Русский

Карта algebraMapInv является левым обратным к algebraMap; то есть algebraMapInv ∘ algebraMap = id_R.

LaTeX

$$$\mathrm{algebraMapInv} \circ \mathrm{algebraMap} = \mathrm{id}_R$$$

Lean4

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

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