R : Type u_2
R₂ : Type ?u.21086
K : Type ?u.21089
M : Type u_1
M₂ : Type ?u.21095
V : Type ?u.21098
S : Type ?u.21101
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x✝ : M
p✝ p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s✝ t : Set M
p : M → Prop
h : x✝ ∈ span R s✝
Hs : ∀ (x : M), x ∈ s✝ → p x
H0 : p 0
H1 : ∀ (x y : M), p x → p y → p (x + y)
H2 : ∀ (a : R) (x : M), p x → p (a • x)
s : Set M
x y : M
⊢ x ∈ p → y ∈ p → x + y ∈ p
R : Type u_2
R₂ : Type ?u.21086
K : Type ?u.21089
M : Type u_1
M₂ : Type ?u.21095
V : Type ?u.21098
S : Type ?u.21101
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x : M
p✝ p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s✝ t : Set M
p : M → Prop
h : x ∈ span R s✝
Hs : ∀ (x : M), x ∈ s✝ → p x
H0 : p 0
H1 : ∀ (x y : M), p x → p y → p (x + y)
H2 : ∀ (a : R) (x : M), p x → p (a • x)
s : Set M
⊢ ∀ {a b : M}, a ∈ p → b ∈ p → a + b ∈ p
intros x y
no goals
R : Type u_2
R₂ : Type ?u.21086
K : Type ?u.21089
M : Type u_1
M₂ : Type ?u.21095
V : Type ?u.21098
S : Type ?u.21101
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x✝ : M
p✝ p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s✝ t : Set M
p : M → Prop
h : x✝ ∈ span R s✝
Hs : ∀ (x : M), x ∈ s✝ → p x
H0 : p 0
H1 : ∀ (x y : M), p x → p y → p (x + y)
H2 : ∀ (a : R) (x : M), p x → p (a • x)
s : Set M
x y : M
⊢ x ∈ p → y ∈ p → x + y ∈ p
exact H1 x y