inverse — Mathlib

English

Analogous result for rTensor: the composition (rTensor.inverse Q hfg hg) ∘ (rTensor Q g) equals mkQ with range of rTensor Q f.

Русский

Аналогично для правого тензора: композиция обратной карты и правого тензора равна mkQ на диапазоне rTensor Q f.

LaTeX

$$inverse_comp_rTensor : (rTensor.inverse Q hfg hg).comp (rTensor Q g) = Submodule.mkQ (p := LinearMap.range (rTensor Q f))$$

Lean4

/-- The inverse map in `rTensor.equiv` -/
noncomputable def inverse : P ⊗[R] Q →ₗ[R] N ⊗[R] Q ⧸ LinearMap.range (rTensor Q f) :=
  rTensor.inverse_of_rightInverse Q hfg (Function.rightInverse_surjInv hg)

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