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