English
If f_i are linear equivalences, congr f is an equivalence whose inverse is given by the componentwise inverses.
Русский
Если каждый f_i — линейное эквивалентство, congr f является эквивалентностью и её обратное задаётся координатно обратными f_i.
LaTeX
$$$\text{congr}\ f\in (\bigotimes_i s_i) \cong (\bigotimes_i t_i)$ with inverse given by coordinatewise inverses$$
Lean4
/-- Let `sᵢ`, `tᵢ` and `t'ᵢ` be families of `R`-modules.
Then there is a function from `⨂ᵢ Hom(sᵢ, Hom(tᵢ, t'ᵢ))` to `Hom(⨂ᵢ sᵢ, Hom(⨂ tᵢ, ⨂ᵢ t'ᵢ))`
defined by `⨂ᵢ fᵢ ↦ ⨂ᵢ aᵢ ↦ ⨂ᵢ bᵢ ↦ ⨂ᵢ fᵢ aᵢ bᵢ`. -/
def piTensorHomMapFun₂ : (⨂[R] i, s i →ₗ[R] t i →ₗ[R] t' i) → (⨂[R] i, s i) →ₗ[R] (⨂[R] i, t i) →ₗ[R] (⨂[R] i, t' i) :=
fun φ => lift <| LinearMap.compMultilinearMap piTensorHomMap <| (lift <| MultilinearMap.piLinearMap <| tprod R) φ
