Commit 2023-10-09 10:41 c4753376

feat(Algebra/DirectSum/Algebra): graded multiplication as a bilinear map (#7577) Also adds some missing actions on GradedMonoid which cleans up the definition of DirectSum.GAlgebra slightly. This also replaces (⟨i, x⟩ : GradedMonoid _) with .mk i x as the former uses Sigma.mk instead of GradedMonoid.mk, which is annoying for rw.