isFG — Mathlib

English

In ModuleCat(R), an object V is FG if and only if V is finitely generated as an R-module, i.e., V has a finite generating set.

Русский

В ModuleCat(R) объект V является FG тогда и только тогда, когда V является конечноп порожденным модулем над R, т.е. имеет конечный множитель-генератор.

LaTeX

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

Lean4

/-- Finitely generated modules, as a property of objects of `ModuleCat R`. -/
def isFG : ObjectProperty (ModuleCat.{v} R) := fun V ↦ Module.Finite R V

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