ι✝ : Type u'
ι' : Type ?u.240558
R : Type u_2
K : Type ?u.240564
M : Type u_3
M' : Type ?u.240570
M'' : Type ?u.240573
V : Type u
V' : Type ?u.240578
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
ι : Type u_1
f : ι → M
hf : LinearIndependent R f
✝ : Nontrivial R
⊢ LinearIndependent R Subtype.val
ι✝ : Type u'
ι' : Type ?u.240558
R : Type u_2
K : Type ?u.240564
M : Type u_3
M' : Type ?u.240570
M'' : Type ?u.240573
V : Type u
V' : Type ?u.240578
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
ι : Type u_1
f : ι → M
hf : LinearIndependent R f
⊢ LinearIndependent R Subtype.val
nontriviality R
no goals
ι✝ : Type u'
ι' : Type ?u.240558
R : Type u_2
K : Type ?u.240564
M : Type u_3
M' : Type ?u.240570
M'' : Type ?u.240573
V : Type u
V' : Type ?u.240578
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
ι : Type u_1
f : ι → M
hf : LinearIndependent R f
✝ : Nontrivial R
⊢ LinearIndependent R Subtype.val
exact (linearIndependent_subtype_range hf.injective).2 hf