Def GradedTensorProduct.of

Modification history

2023-12-18 04:13

Mathlib/LinearAlgebra/TensorProduct/Graded/Internal.lean

feat: the graded tensor product (#7394) …

Added GradedTensorProduct.of View on Github →