iSupIndep_iff_dfinsuppSumAddHom_injective

English

If iSupIndep holds for p, then the sumAddHom map is injective.

Русский

Если iSupIndep выполняется для p, то sumAddHom инъективно.

LaTeX

$$iSupIndep p → Injective (sumAddHom fun i => (p i).subtype)$$

Lean4

/-- A family of additive subgroups over an additive group are independent if and only if
`DFinsupp.sumAddHom` applied with `AddSubgroup.subtype` is injective. -/
theorem iSupIndep_iff_dfinsuppSumAddHom_injective (p : ι → AddSubgroup N) :
    iSupIndep p ↔ Function.Injective (sumAddHom fun i => (p i).subtype) :=
  ⟨iSupIndep.dfinsuppSumAddHom_injective, iSupIndep_of_dfinsuppSumAddHom_injective' p⟩

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