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 (s • t)
x : A
hx : x ∈ s • t
p : S
q : A
_hp : p ∈ s
hq : q ∈ t
hpq : p • q = x
⊢ k • x ∈ 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 (s • t)
x : A
hx : x ∈ s • t
⊢ k • x ∈ span R (s • t)
let ⟨p, q, _hp, hq, hpq⟩ := Set.mem_smul.1 hx
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 (s • t)
x : A
hx : x ∈ s • t
p : S
q : A
_hp : p ∈ s
hq : q ∈ t
hpq : p • q = x
⊢ (k * p) • q ∈ 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 (s • t)
x : A
hx : x ∈ s • t
p : S
q : A
_hp : p ∈ s
hq : q ∈ t
hpq : p • q = x
⊢ k • x ∈ span R (s • t)
rw [← hpq, smul_smul]
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 (s • t)
x : A
hx : x ∈ s • t
p : S
q : A
_hp : p ∈ s
hq : q ∈ t
hpq : p • q = x
⊢ (k * p) • q ∈ span R (s • t)
exact smul_mem_span_smul_of_mem (hs.symm ▸ mem_top) hq
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 (s • 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 (s • 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 (s • 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 (s • 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 (s • 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 (s • 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