English
The subtype of any subset t with appropriate closure carries a module structure over S.
Русский
Подтип любой подмножества t со соответствующей замкнутостью имеет модульную структуру над S.
LaTeX
$$Module' {T} : Subtype fun x => SetLike.instMembership.mem T x → Module S (Subtype fun x => SetLike.instMembership.mem T x)$$
Lean4
instance (priority := 75) module' {T : Type*} [Semiring R] [AddCommMonoid M] [Semiring S] [Module R M] [SMul S R]
[Module S M] [IsScalarTower S R M] [SetLike T M] [AddSubmonoidClass T M] [SMulMemClass T R M] (t : T) : Module S t
where
one_smul _ := by ext; simp
mul_smul _ _ _ := by ext; simp [mul_smul]
smul_zero _ := by ext; simp
zero_smul _ := by ext; simp
add_smul _ _ _ := by ext; simp [add_smul]
smul_add _ _ _ := by ext; simp [smul_add]
