Def TensorProduct.gradedCommAux

Modification history

2026-03-25 04:00

Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean

chore(DirectSum): clean up instances (#37135) …

Modified TensorProduct.gradedCommAux View on Github →

2023-12-18 04:13

Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean

feat: the graded tensor product (#7394) …

Added TensorProduct.gradedCommAux View on Github →