ι : Type u_2
R : Type ?u.535889
S : Type ?u.535892
M : ι → Type ?u.535897
N : Type u_1
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → AddSubmonoid N
h : Function.Injective ↑(sumAddHom fun i => AddSubmonoid.subtype (p i))
⊢ Independent (↑AddSubmonoid.toNatSubmodule ∘ p)
ι : Type u_2
R : Type ?u.535889
S : Type ?u.535892
M : ι → Type ?u.535897
N : Type u_1
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → AddSubmonoid N
h : Function.Injective ↑(sumAddHom fun i => AddSubmonoid.subtype (p i))
⊢ Independent p
rw [← independent_map_orderIso_iff (AddSubmonoid.toNatSubmodule : AddSubmonoid N ≃o _)]
no goals
ι : Type u_2
R : Type ?u.535889
S : Type ?u.535892
M : ι → Type ?u.535897
N : Type u_1
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → AddSubmonoid N
h : Function.Injective ↑(sumAddHom fun i => AddSubmonoid.subtype (p i))
⊢ Independent (↑AddSubmonoid.toNatSubmodule ∘ p)
exact independent_of_dfinsupp_lsum_injective _ h