Def DirectSum.gMulLHom

Modification history

2023-10-09 10:41

Mathlib/Algebra/DirectSum/Algebra.lean

feat(Algebra/DirectSum/Algebra): graded multiplication as a bilinear map (#7577) …

Added DirectSum.gMulLHom View on Github →