Def TensorProduct.piRightInv

Modification history

2024-11-14 06:25

Mathlib/LinearAlgebra/TensorProduct/Pi.lean

feat(Algebra/TensorProduct): tensor product commutes with finite products (#18635)

Added TensorProduct.piRightInv View on Github →