addSubgroup_iSupIndep

Mathlib.Algebra.DirectSum.Module

URI: https://scilib.ai/kg/mathlib#DirectSum.IsInternal.addSubgroup_iSupIndep

← MathLib Explorer

English

If h: IsInternal A for AddSubmonoid family A, then iSupIndep A.

Русский

Если A : ι → AddSubmonoid имеет свойства IsInternal, тогда A является iSupIndep.

LaTeX

$$IsInternal A \Rightarrow iSupIndep A$$

Lean4

theorem addSubgroup_iSupIndep {G : Type*} [AddCommGroup G] {A : ι → AddSubgroup G} (h : IsInternal A) : iSupIndep A :=
  iSupIndep_of_dfinsuppSumAddHom_injective' _ h.injective

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru