Commit 2023-12-23 00:28 c56af57a

View on Github →

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

Estimated changes

Modified Mathlib/Algebra/GradedMonoid.lean

added theorem GradedMonoid.fst_mul

added theorem GradedMonoid.fst_one

added theorem GradedMonoid.fst_pow

added theorem GradedMonoid.fst_smul

modified def GradedMonoid.mkZeroMonoidHom

modified theorem GradedMonoid.smul_mk

added theorem GradedMonoid.snd_mul

added theorem GradedMonoid.snd_one

added theorem GradedMonoid.snd_pow

added theorem GradedMonoid.snd_smul