inverse_comp_rTensor — Mathlib

English

The inverse composition result for rTensor states that the appropriate inverse composed with rTensor g yields the mkQ map for the right tensor.

Русский

Свойство обратной композиции для правого тензора говорит об образовании карты mkQ через обратное отображение.

LaTeX

$$inverse_apply (y) = mk y$$

Lean4

theorem inverse_comp_rTensor :
    (rTensor.inverse Q hfg hg).comp (rTensor Q g) = Submodule.mkQ (p := LinearMap.range (rTensor Q f)) := by
  rw [rTensor.inverse, rTensor.inverse_of_rightInverse_comp_rTensor]

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