R : Type u_2
R₂ : Type ?u.123041
K : Type ?u.123044
M : Type u_1
M₂ : Type ?u.123050
V : Type ?u.123053
S : Type ?u.123056
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
x : M
⊢ (∀ (v : M), v ∈ ⊤ → ∃ r, r • x = v) ↔ ∀ (v : M), ∃ r, r • x = v
R : Type u_2
R₂ : Type ?u.123041
K : Type ?u.123044
M : Type u_1
M₂ : Type ?u.123050
V : Type ?u.123053
S : Type ?u.123056
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
x : M
⊢ span R {x} = ⊤ ↔ ∀ (v : M), ∃ r, r • x = v
rw [eq_top_iff, le_span_singleton_iff]
no goals
R : Type u_2
R₂ : Type ?u.123041
K : Type ?u.123044
M : Type u_1
M₂ : Type ?u.123050
V : Type ?u.123053
S : Type ?u.123056
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
x : M
⊢ (∀ (v : M), v ∈ ⊤ → ∃ r, r • x = v) ↔ ∀ (v : M), ∃ r, r • x = v
tauto