module_finite

Mathlib.Algebra.Module.ZLattice.Basic

URI: https://scilib.ai/kg/mathlib#ZLattice.module_finite

English

The module finitely generated property extends through an isomorphism to real vector space contexts.

Русский

Свойство конечной порожденности модуля сохраняется при преобразовании к вещественному контексту.

LaTeX

$$$\text{Module.Finite} \mathbb{Z} L$$$

Lean4

theorem module_finite [IsZLattice K L] : Module.Finite ℤ L :=
  Module.Finite.iff_fg.mpr (ZLattice.FG K L)

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

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

Разделы

Аффилиация

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