isFG_iff — Mathlib

English

For a ring R and a module V, FG-structure is equivalent to finiteness: isFG R V holds exactly when V is finite as an R-module.

Русский

Для кольца R и модуля V условие FG эквивалентно конечности: isFG R V верно тогда и только тогда V является конечным как R-модуль.

LaTeX

$$$isFG\\;R\\;V \\iff Module.Finite\\;R\\;V$$$

Lean4

theorem isFG_iff (V : ModuleCat.{v} R) : isFG R V ↔ Module.Finite R V :=
  Iff.rfl

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