English
For a graded monoid A, given r, r', and a condition H, the nth coordinate of the product r * of_i r' equals r_j · r' when the condition holds, else 0.
Русский
Для градуированной моноида A, если заданы r, r' и условие H, коэффициент в позиции n равен r_j · r' при выполнении условия, иначе 0.
LaTeX
$$$$\\big[\\text{Given } r, r', H:\\forall x, x+i=n \\iff x=j\\big] \quad (r * \\mathrm{of}(A,i)\\; r')_n = r_j \\cdot r'. $$$$
Lean4
/-- The supremum of submodules that form a graded monoid is a subalgebra, and equal to the range of
`DirectSum.coeAlgHom`. -/
theorem iSup_eq_toSubmodule_range [AddMonoid ι] [CommSemiring S] [Semiring R] [Algebra S R] (A : ι → Submodule S R)
[SetLike.GradedMonoid A] : ⨆ i, A i = Subalgebra.toSubmodule (DirectSum.coeAlgHom A).range :=
(Submodule.iSup_eq_range_dfinsupp_lsum A).trans <| SetLike.coe_injective rfl
