R : Type u_2
R₂ : Type ?u.329641
K : Type ?u.329644
M : Type u_1
M₂ : Type ?u.329650
V : Type ?u.329653
S : Type ?u.329656
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
⊢ y ∈ span R {x} ↔ ∃ y_1, ↑(toSpanSingleton R M x) y_1 = y
R : Type u_2
R₂ : Type ?u.329641
K : Type ?u.329644
M : Type u_1
M₂ : Type ?u.329650
V : Type ?u.329653
S : Type ?u.329656
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
⊢ y ∈ span R {x} ↔ y ∈ range (toSpanSingleton R M x)
refine' Iff.trans _ LinearMap.mem_range.symm
no goals
R : Type u_2
R₂ : Type ?u.329641
K : Type ?u.329644
M : Type u_1
M₂ : Type ?u.329650
V : Type ?u.329653
S : Type ?u.329656
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
⊢ y ∈ span R {x} ↔ ∃ y_1, ↑(toSpanSingleton R M x) y_1 = y
exact mem_span_singleton