English
From a structure S that is a SetLike AddSubmonoidClass and SMulMemClass, one builds a Submodule whose carrier is S.
Русский
Из структуры S типа SetLike AddSubmonoidClass и SMulMemClass строится подмодуль, носителем которого является S.
LaTeX
$$$S \\mapsto \\text{Submodule}(R,M) \\text{ с носителем } S$$$
Lean4
/-- The actual `Submodule` obtained from an element of a `SMulMemClass` and `AddSubmonoidClass`. -/
@[simps]
def ofClass {S R M : Type*} [Semiring R] [AddCommMonoid M] [Module R M] [SetLike S M] [AddSubmonoidClass S M]
[SMulMemClass S R M] (s : S) : Submodule R M where
carrier := s
add_mem' := add_mem
zero_mem' := zero_mem _
smul_mem' := SMulMemClass.smul_mem
