ι : Type u'
ι' : Type ?u.213479
R : Type u_2
K : Type ?u.213485
M : Type u_1
M' : Type ?u.213491
M'' : Type ?u.213494
V : Type u
V' : Type ?u.213499
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
t s : Set M
h : t ⊆ s
⊢ Disjoint (Finsupp.supported R R s) (LinearMap.ker (Finsupp.total M M R id)) →
    Disjoint (Finsupp.supported R R t) (LinearMap.ker (Finsupp.total M M R id))
ι : Type u'
ι' : Type ?u.213479
R : Type u_2
K : Type ?u.213485
M : Type u_1
M' : Type ?u.213491
M'' : Type ?u.213494
V : Type u
V' : Type ?u.213499
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
t s : Set M
h : t ⊆ s
⊢ (LinearIndependent R fun x => ↑x) → LinearIndependent R fun x => ↑x
simp only [linearIndependent_subtype_disjoint]
no goals
ι : Type u'
ι' : Type ?u.213479
R : Type u_2
K : Type ?u.213485
M : Type u_1
M' : Type ?u.213491
M'' : Type ?u.213494
V : Type u
V' : Type ?u.213499
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
t s : Set M
h : t ⊆ s
⊢ Disjoint (Finsupp.supported R R s) (LinearMap.ker (Finsupp.total M M R id)) →
    Disjoint (Finsupp.supported R R t) (LinearMap.ker (Finsupp.total M M R id))
exact Disjoint.mono_left (Finsupp.supported_mono h)