IsFiniteLength

Mathlib.RingTheory.FiniteLength

URI: https://scilib.ai/kg/mathlib#IsFiniteLength

Lean4

/-- A module of finite length is either trivial or a simple extension of a module known
to be of finite length. -/
inductive IsFiniteLength : ∀ (M : Type*) [AddCommGroup M] [Module R M], Prop
  | of_subsingleton {M} [AddCommGroup M] [Module R M] [Subsingleton M] : IsFiniteLength M
  |
  of_simple_quotient {M} [AddCommGroup M] [Module R M] {N : Submodule R M} [IsSimpleModule R (M ⧸ N)] :
    IsFiniteLength N → IsFiniteLength M

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

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

Разделы

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

Аффилиация

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