fg_top — Mathlib

English

For any submodule N of M, (⊤ : Submodule R N).FG is equivalent to N.FG.

Русский

Для любого подподмодуля N модуля M верно: FG(⊤_N) ⇔ FG(N).

LaTeX

$$(⊤ : Submodule R N).FG ↔ N.FG$$

Lean4

theorem fg_top (N : Submodule R M) : (⊤ : Submodule R N).FG ↔ N.FG :=
  ⟨fun h => N.range_subtype ▸ map_top N.subtype ▸ h.map _, fun h =>
    fg_of_fg_map_injective N.subtype Subtype.val_injective <| by rwa [map_top, range_subtype]⟩

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