submodule_iSupIndep — Mathlib

English

If A is a collection of submodules indexed by ι and an internal direct sum, then the submodules are independently arranged along the index.

Русский

Если A — набор подмодулов, образующий внутреннее разложение, то компоненты индексной системы независимы друг относительно друга.

LaTeX

$$IsInternal A ⇒ iSupIndep A$$

Lean4

/-- If a direct sum of submodules is internal then the submodules are independent. -/
theorem submodule_iSupIndep (h : IsInternal A) : iSupIndep A :=
  iSupIndep_of_dfinsupp_lsum_injective _ h.injective

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