English
When f,g are exact and h is a right inverse of g, many congruence lemmas hold: congr_simp shows equality of two forms of lTensor inverse; congruence relations hold for the equivalences and maps involved.
Русский
При точности f и g и наличии правого обратного h существуют леммы эквивалентности и конгруэнтности между соответствующими отображениями.
LaTeX
$$congr_simp : Eq (lTensor.inverse_of_rightInverse Q hfg hgh) (lTensor.inverse_of_rightInverse Q ⋯ ⋯)$$
Lean4
/-- For a surjective `f : N →ₗ[R] P`,
the natural equivalence between `N ⊗[R] Q ⧸ (range (rTensor Q f))` and `P ⊗[R] Q` -/
noncomputable def equiv : ((N ⊗[R] Q) ⧸ (LinearMap.range (rTensor Q f))) ≃ₗ[R] (P ⊗[R] Q) :=
rTensor.linearEquiv_of_rightInverse Q hfg (Function.rightInverse_surjInv hg)
