finite

Mathlib.Algebra.Module.Presentation.Finite

URI: https://scilib.ai/kg/mathlib#Module.Presentation.finite

English

If a presentation pres has a finite generating set G, then the underlying module M is finite.

Русский

Если презентация pres имеет конечный порождающий набор G, тогда связанный модуль M конечен.

LaTeX

$$[Finite pres.G] → Module.Finite A M$$

Lean4

theorem finite [Finite pres.G] : Module.Finite A M :=
  Finite.of_surjective _ pres.surjective_π

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

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

Разделы

Аффилиация

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