English
If ι is an additive monoid and A is a graded monoid over ι, then GradedMonoid A carries a natural monoid structure; the multiplication and unit are inherited from the graded product.
Русский
Если ι — аддитивный моноид, и A — градуированный моноид по ι, тогда GradedMonoid A естественным образом образует моноид: умножение и единица задаются градуированным произведением.
LaTeX
$$$\\operatorname{Monoid}(\\mathrm{GradedMonoid} A)$$$
Lean4
/-- `GMonoid` implies a `Monoid (GradedMonoid A)`. -/
instance toMonoid [AddMonoid ι] [GMonoid A] : Monoid (GradedMonoid A)
where
one := 1
mul := (· * ·)
npow n a := GradedMonoid.mk _ (GMonoid.gnpow n a.snd)
npow_zero a := GMonoid.gnpow_zero' a
npow_succ n a := GMonoid.gnpow_succ' n a
one_mul := GMonoid.one_mul
mul_one := GMonoid.mul_one
mul_assoc := GMonoid.mul_assoc
