English
The set of all homogeneous elements forms a submonoid of the ambient monoid R: it contains 1 and is closed under multiplication.
Русский
Множество однородных элементов образует подмоноид окружного моноида R: содержит 1 и замкнуто относительно умножения.
LaTeX
$$$ \{a \in R \mid \exists i, a \in A(i)\} \leqslant R \\text{and } 1 \in \{a \mid \exists i, a \in A(i)\} ,\; \forall a,b \in \{a \mid \exists i, a \in A(i)\}, ab \in \{a \mid \exists i, a \in A(i)\} $$$
Lean4
/-- When `A` is a `SetLike.GradedMonoid A`, then the homogeneous elements forms a submonoid. -/
def homogeneousSubmonoid [AddMonoid ι] [Monoid R] (A : ι → S) [SetLike.GradedMonoid A] : Submonoid R
where
carrier := {a | SetLike.IsHomogeneousElem A a}
one_mem' := SetLike.isHomogeneousElem_one A
mul_mem' a b := SetLike.IsHomogeneousElem.mul a b
