Theorem TensorProduct.gradedComm_algebraMap_tmul

Modification history

2025-04-13 20:41
Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean
feat: generalize Mathlib.LinearAlgebra (#23179) …
Modified TensorProduct.gradedComm_algebraMap_tmulView on Github →
2024-08-08 02:10
Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean
chore: backports for leanprover/lean4#4814 (part 32) (#15577)
Modified TensorProduct.gradedComm_algebraMap_tmulView on Github →
2023-12-18 04:13
Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean
feat: the graded tensor product (#7394) …
Added TensorProduct.gradedComm_algebraMap_tmulView on Github →