English
A variant: the map of a list under graded Monoid, then prod equals the mk of a dProd from the components.
Русский
Вариант: отображение списка через graded Monoid, затем произведение равно mk от dProd из компонент.
LaTeX
$$$(l.map f).prod = \\mathrm{GradedMonoid.mk} _ (l.dProd (\\lambda i . (f i).1) (\\lambda i . (f i).2))$$$
Lean4
/-- If all grades are the same type and themselves form a monoid, then there is a trivial grading
structure. -/
@[simps gnpow]
instance gMonoid [AddMonoid ι] [Monoid R] : GradedMonoid.GMonoid fun _ : ι => R :=
-- { Mul.gMul ι, One.gOne ι with
{ One.gOne ι with
mul := fun x y => x * y
one_mul := fun _ => Sigma.ext (zero_add _) (heq_of_eq (one_mul _))
mul_one := fun _ => Sigma.ext (add_zero _) (heq_of_eq (mul_one _))
mul_assoc := fun _ _ _ => Sigma.ext (add_assoc _ _ _) (heq_of_eq (mul_assoc _ _ _))
gnpow := fun n _ a => a ^ n
gnpow_zero' := fun _ => Sigma.ext (zero_nsmul _) (heq_of_eq (Monoid.npow_zero _))
gnpow_succ' := fun _ ⟨_, _⟩ => Sigma.ext (succ_nsmul _ _) (heq_of_eq (Monoid.npow_succ _ _)) }
