R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid A
inst✝⁴ : Module R S
inst✝³ : Module S A
inst✝² : Module R A
inst✝¹ : IsScalarTower R S A
inst✝ : SMulCommClass R S A
s : Set S
hs : span R s = ⊤
t : Set A
k : S
x : A
hx : x ∈ span R t
⊢ 0 ∈ span R (s • t)
R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid A
inst✝⁴ : Module R S
inst✝³ : Module S A
inst✝² : Module R A
inst✝¹ : IsScalarTower R S A
inst✝ : SMulCommClass R S A
s : Set S
hs : span R s = ⊤
t : Set A
k : S
x : A
hx : x ∈ span R t
⊢ k • 0 ∈ span R (s • t)
rw [smul_zero]
no goals
R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid A
inst✝⁴ : Module R S
inst✝³ : Module S A
inst✝² : Module R A
inst✝¹ : IsScalarTower R S A
inst✝ : SMulCommClass R S A
s : Set S
hs : span R s = ⊤
t : Set A
k : S
x : A
hx : x ∈ span R t
⊢ 0 ∈ span R (s • t)
exact zero_mem _
R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid A
inst✝⁴ : Module R S
inst✝³ : Module S A
inst✝² : Module R A
inst✝¹ : IsScalarTower R S A
inst✝ : SMulCommClass R S A
s : Set S
hs : span R s = ⊤
t : Set A
k : S
x✝ : A
hx : x✝ ∈ span R t
x y : A
ihx : k • x ∈ span R (s • t)
ihy : k • y ∈ span R (s • t)
⊢ k • x + k • y ∈ span R (s • t)
R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid A
inst✝⁴ : Module R S
inst✝³ : Module S A
inst✝² : Module R A
inst✝¹ : IsScalarTower R S A
inst✝ : SMulCommClass R S A
s : Set S
hs : span R s = ⊤
t : Set A
k : S
x✝ : A
hx : x✝ ∈ span R t
x y : A
ihx : k • x ∈ span R (s • t)
ihy : k • y ∈ span R (s • t)
⊢ k • (x + y) ∈ span R (s • t)
rw [smul_add]
no goals
R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid A
inst✝⁴ : Module R S
inst✝³ : Module S A
inst✝² : Module R A
inst✝¹ : IsScalarTower R S A
inst✝ : SMulCommClass R S A
s : Set S
hs : span R s = ⊤
t : Set A
k : S
x✝ : A
hx : x✝ ∈ span R t
x y : A
ihx : k • x ∈ span R (s • t)
ihy : k • y ∈ span R (s • t)
⊢ k • x + k • y ∈ span R (s • t)
exact add_mem ihx ihy