Commit 2025-04-30 12:12 d8c00d34
View on Github →feat(LinearAlgebra/PiTensorProduct): dependent version of tmulEquiv (#18534)
Given a family of R-modules N indexed by ι ⊕ ι', we obtain a linear equivalence tmulEquivDep : (⨂[R] i₁, N (.inl i₁)) ⊗[R] (⨂[R] i₂, N (.inr i₂)) ≃ₗ[R] ⨂[R] i, N i, which generalizes tmulEquiv (which is the case all N i are the same module).