R : Type u_2
R₂ : Type ?u.12510
K : Type ?u.12513
M : Type u_1
M₂ : Type ?u.12519
V : Type ?u.12522
S : Type ?u.12525
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
⊢ span R (insert 0 s) ≤ span R s
R : Type u_2
R₂ : Type ?u.12510
K : Type ?u.12513
M : Type u_1
M₂ : Type ?u.12519
V : Type ?u.12522
S : Type ?u.12525
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
⊢ span R (insert 0 s) = span R s
refine' le_antisymm _ (Submodule.span_mono (Set.subset_insert 0 s))
R : Type u_2
R₂ : Type ?u.12510
K : Type ?u.12513
M : Type u_1
M₂ : Type ?u.12519
V : Type ?u.12522
S : Type ?u.12525
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
⊢ 0 ∈ ↑(span R s) ∧ s ⊆ ↑(span R s)
R : Type u_2
R₂ : Type ?u.12510
K : Type ?u.12513
M : Type u_1
M₂ : Type ?u.12519
V : Type ?u.12522
S : Type ?u.12525
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
⊢ span R (insert 0 s) ≤ span R s
rw [span_le, Set.insert_subset]
no goals
R : Type u_2
R₂ : Type ?u.12510
K : Type ?u.12513
M : Type u_1
M₂ : Type ?u.12519
V : Type ?u.12522
S : Type ?u.12525
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
⊢ 0 ∈ ↑(span R s) ∧ s ⊆ ↑(span R s)
exact ⟨by simp only [SetLike.mem_coe, Submodule.zero_mem], Submodule.subset_span⟩
no goals
R : Type u_2
R₂ : Type ?u.12510
K : Type ?u.12513
M : Type u_1
M₂ : Type ?u.12519
V : Type ?u.12522
S : Type ?u.12525
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
⊢ 0 ∈ ↑(span R s)
simp only [SetLike.mem_coe, Submodule.zero_mem]