English
If the direct-sum construction via sumAddHom is injective for a family of additive subgroups, then the family is iSupIndep (independent).
Русский
Если отображение sumAddHom, применённое к семейству добавочно подгрупп, инъективно, то семейство независимо (iSupIndep).
LaTeX
$$$\text{If } (p_i)_{i\in I} \text{ are subgroups with } p_i \le N,\quad \text{and } \operatorname{sumAddHom} (\,\cdot\,)(p_i) \text{ is injective, then } i\!\text{SupIndep } p.$$$
Lean4
/-- If `DFinsupp.sumAddHom` applied with `AddSubmonoid.subtype` is injective then the additive
subgroups are independent. -/
theorem iSupIndep_of_dfinsuppSumAddHom_injective' (p : ι → AddSubgroup N)
(h : Function.Injective (sumAddHom fun i => (p i).subtype)) : iSupIndep p :=
by
rw [← iSupIndep_map_orderIso_iff (AddSubgroup.toIntSubmodule : AddSubgroup N ≃o _)]
exact iSupIndep_of_dfinsupp_lsum_injective _ h
