Def GradedTensorProduct.includeLeft

Modification history

2023-12-18 04:13

Mathlib/LinearAlgebra/TensorProduct/Graded/Internal.lean

feat: the graded tensor product (#7394) …

Added GradedTensorProduct.includeLeft View on Github →