Theorem GradedMonoid.smul_mk

Modification history

2023-12-23 00:28
Mathlib/Algebra/GradedMonoid.lean
feat(Algebra/GradedMonoid): missing lemmas about `fst` and `snd` (#9227)
Modified GradedMonoid.smul_mkView on Github →
2023-10-09 10:41
Mathlib/Algebra/GradedMonoid.lean
feat(Algebra/DirectSum/Algebra): graded multiplication as a bilinear map (#7577) …
Added GradedMonoid.smul_mkView on Github →