inverse_comp_lTensor — Mathlib

English

The theorem asserts that the composition (lTensor.inverse Q hfg hgh) ∘ (LinearMap.lTensor Q g) equals the canonical map to the quotient (the Q⊗N mod range f), i.e., the projection mkQ.

Русский

Состав обратной карты и левого тензорного отображения равен каноническому карте к фактор-модулю.

LaTeX

$$$(lTensor.inverse Q hfg hgh) ∘ (LinearMap.lTensor Q g) = \\mathrm{mkQ} (p := \\mathrm{range}(lTensor Q f))$$$

Lean4

theorem inverse_comp_lTensor :
    (lTensor.inverse Q hfg hg).comp (lTensor Q g) = Submodule.mkQ (p := LinearMap.range (lTensor Q f)) := by
  rw [lTensor.inverse, lTensor.inverse_of_rightInverse_comp_lTensor]

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