submodule_iSup_eq_top — Mathlib

English

Over a ring, the two prior notions (iSupIndep and iSup) provide an equivalence giving an internal decomposition.

Русский

Для кольца существует эквивалентность, связывающая независимость iSupIndep и верхний предел iSup с внутренним разложением.

LaTeX

$$IsInternal A ↔ iSupIndep A ∧ iSup A = ⊤$$

Lean4

/-- If a direct sum of submodules is internal then the submodules span the module. -/
theorem submodule_iSup_eq_top (h : IsInternal A) : iSup A = ⊤ :=
  by
  rw [Submodule.iSup_eq_range_dfinsupp_lsum, LinearMap.range_eq_top]
  exact Function.Bijective.surjective h

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