ι : Type u'
ι' : Type ?u.632452
R : Type u_2
K : Type ?u.632458
M : Type u_1
M' : Type u_3
M'' : Type ?u.632467
V : Type u
V' : Type ?u.632472
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
s : Set M
f : M →ₗ[R] M'
hs : LinearIndependent R fun x => ↑x
hf_inj : Disjoint (span R (Set.range Subtype.val)) (ker f)
⊢ LinearIndependent R fun x => ↑x
ι : Type u'
ι' : Type ?u.632452
R : Type u_2
K : Type ?u.632458
M : Type u_1
M' : Type u_3
M'' : Type ?u.632467
V : Type u
V' : Type ?u.632472
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
s : Set M
f : M →ₗ[R] M'
hs : LinearIndependent R fun x => ↑x
hf_inj : Disjoint (span R s) (ker f)
⊢ LinearIndependent R fun x => ↑x
rw [← @Subtype.range_coe _ s] at hf_inj
ι : Type u'
ι' : Type ?u.632452
R : Type u_2
K : Type ?u.632458
M : Type u_1
M' : Type u_3
M'' : Type ?u.632467
V : Type u
V' : Type ?u.632472
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
s : Set M
f : M →ₗ[R] M'
hs : LinearIndependent R fun x => ↑x
hf_inj : Disjoint (span R (Set.range Subtype.val)) (ker f)
⊢ Set.range (↑f ∘ fun x => ↑x) = ↑f '' s
ι : Type u'
ι' : Type ?u.632452
R : Type u_2
K : Type ?u.632458
M : Type u_1
M' : Type u_3
M'' : Type ?u.632467
V : Type u
V' : Type ?u.632472
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
s : Set M
f : M →ₗ[R] M'
hs : LinearIndependent R fun x => ↑x
hf_inj : Disjoint (span R (Set.range Subtype.val)) (ker f)
⊢ LinearIndependent R fun x => ↑x
refine' (hs.map hf_inj).to_subtype_range' _
no goals
ι : Type u'
ι' : Type ?u.632452
R : Type u_2
K : Type ?u.632458
M : Type u_1
M' : Type u_3
M'' : Type ?u.632467
V : Type u
V' : Type ?u.632472
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
s : Set M
f : M →ₗ[R] M'
hs : LinearIndependent R fun x => ↑x
hf_inj : Disjoint (span R (Set.range Subtype.val)) (ker f)
⊢ Set.range (↑f ∘ fun x => ↑x) = ↑f '' s
simp [Set.range_comp f]