Theorem GradedMonoid.fst_smul

Modification history

2023-12-23 00:28

Mathlib/Algebra/GradedMonoid.lean

feat(Algebra/GradedMonoid): missing lemmas about `fst` and `snd` (#9227)

Added GradedMonoid.fst_smul View on Github →