Def GradedTensorProduct

Modification history

2023-12-18 04:13

Mathlib/LinearAlgebra/TensorProduct/Graded/Internal.lean

feat: the graded tensor product (#7394) …

Added GradedTensorProduct View on Github →