rTensorInv_leftInverse — Mathlib

English

The left inverse property holds: the composition of rTensorInv with rTensorHom is the identity on the appropriate space.

Русский

Свойство левого обратного: композиция rTensorInv и rTensorHom равна тождественному отображению.

LaTeX

$$$(rTensorInv P Q e) \\circ (rTensorHom M) = \\mathrm{id}$$$

Lean4

theorem rTensorInv_leftInverse : Function.LeftInverse (rTensorInv P Q e) (.rTensorHom M) := fun _ ↦
  by
  simp_rw [rTensorInv, LinearEquiv.coe_trans, LinearMap.comp_apply, LinearEquiv.coe_toLinearMap]
  rw [← LinearEquiv.eq_symm_apply]
  ext; simp [LinearEquiv.congrLeft, LinearEquiv.congrRight, LinearEquiv.arrowCongrAddEquiv]

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