Theorem TensorProduct.piRight_symm_single

Modification history

2024-11-14 06:25
Mathlib/LinearAlgebra/TensorProduct/Pi.lean
feat(Algebra/TensorProduct): tensor product commutes with finite products (#18635)
Added TensorProduct.piRight_symm_singleView on Github →