dfinsuppSumAddHom_injective — Mathlib

English

The canonical map from the direct sum of additive subgroups to N is injective when the subgroups are iSupIndep.

Русский

Каноническое отображение из прямой суммы аддитивных подгрупп в N инъективно при iSupIndep.

LaTeX

$$$iSupIndep p \rightarrow \text{Injective } (\sumAddHom (\lambda i . (p i).subtype))$$$

Lean4

/-- The canonical map out of a direct sum of a family of additive subgroups is injective when the
additive subgroups are `iSupIndep`. -/
theorem dfinsuppSumAddHom_injective {p : ι → AddSubgroup N} (h : iSupIndep p) :
    Function.Injective (sumAddHom fun i => (p i).subtype) :=
  by
  rw [← iSupIndep_map_orderIso_iff (AddSubgroup.toIntSubmodule : AddSubgroup N ≃o _)] at h
  exact h.dfinsupp_lsum_injective

Похожие утверждения