iff_fg — Mathlib

English

For a submodule N ≤ M, M finite over R is equivalent to N being FG (finitely generated).

Русский

Для подмодуля N ≤ M финитность M над R эквивалентна тому, что N является FG (конечнопоряженным порождением).

LaTeX

$$$\\forall N \\le M,\\; Module.Finite\\; R\\; N \\iff N.FG$$$

Lean4

theorem iff_fg {N : Submodule R M} : Module.Finite R N ↔ N.FG :=
  Module.finite_def.trans N.fg_top

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