ι : Type u_2
R : Type ?u.632921
S : Type ?u.632924
M : ι → Type ?u.632929
N : Type u_1
dec_ι : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → AddSubgroup N
h : Function.Injective ↑(sumAddHom fun i => AddSubgroup.subtype (p i))
⊢ Independent (↑AddSubgroup.toIntSubmodule ∘ p)
ι : Type u_2
R : Type ?u.632921
S : Type ?u.632924
M : ι → Type ?u.632929
N : Type u_1
dec_ι : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → AddSubgroup N
h : Function.Injective ↑(sumAddHom fun i => AddSubgroup.subtype (p i))
⊢ Independent p
rw [← independent_map_orderIso_iff (AddSubgroup.toIntSubmodule : AddSubgroup N ≃o _)]
no goals
ι : Type u_2
R : Type ?u.632921
S : Type ?u.632924
M : ι → Type ?u.632929
N : Type u_1
dec_ι : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → AddSubgroup N
h : Function.Injective ↑(sumAddHom fun i => AddSubgroup.subtype (p i))
⊢ Independent (↑AddSubgroup.toIntSubmodule ∘ p)
exact independent_of_dfinsupp_lsum_injective _ h