English
Independence of a family of submodules is equivalent to the injectivity of the lsum map built from their subtypes.
Русский
Независимость семейства подмодулей эквивалентна инъективности отображения lsum, построенного из подтипов подмодулей.
LaTeX
$$$iSupIndep\ p \;\iff\; (lsum\ ℕ \; (\lambda i . (p i).subtype)) \text{ is injective}$$$
Lean4
/-- A family of submodules over an additive group are independent if and only iff `DFinsupp.lsum`
applied with `Submodule.subtype` is injective.
Note that this is not generally true for `[Semiring R]`; see
`iSupIndep.dfinsupp_lsum_injective` for details. -/
theorem iSupIndep_iff_dfinsupp_lsum_injective (p : ι → Submodule R N) :
iSupIndep p ↔ Function.Injective (lsum ℕ fun i => (p i).subtype) :=
⟨iSupIndep.dfinsupp_lsum_injective, iSupIndep_of_dfinsupp_lsum_injective p⟩
