Theorem TensorProduct.gradedComm_tmul_one

Modification history

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