English
Let M be an additive commutative monoid with a compatible order and an R-module structure, and let S be a submodule of M. Then S inherits the structure of an ordered additive monoid from M; i.e., S is an ordered additive monoid under the inherited addition and order.
Русский
Пусть M – упорядоченная коммутативная аддитивная моноида, обладающая структурой модуля над R, и S — подмодуль M. Тогда S наследует структуру упорядоченного аддитивного моноида: подмодульS является упорядоченным аддитивным моноидом с тем же доделанным порядком и операцией сложения.
LaTeX
$$$\forall (R,M)\,[\text{Semiring } R]\ [\text{AddCommMonoid } M]\ [\text{PartialOrder } M]\ [\text{IsOrderedAddMonoid } M]\ [\text{Module } R M]\ (S : Submodule\ R\ M),\ IsOrderedAddMonoid\ S$$$
Lean4
/-- A submodule of an ordered additive monoid is an ordered additive monoid. -/
instance toIsOrderedAddMonoid [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] [Module R M]
(S : Submodule R M) : IsOrderedAddMonoid S :=
Function.Injective.isOrderedAddMonoid Subtype.val (fun _ _ => rfl) .rfl
