fg_of_localized_maximal — Mathlib

English

If two submodules have identical localizations at all maximal ideals, they are equal.

Русский

Если две подмодули совпадают после локализации по всем макс. идеалам, они равны.

LaTeX

$$$\\forall P [P.IsMaximal], N_1.localized_0 P.primeCompl (f P) = N_2.localized_0 P.primeCompl (f P) \\Rightarrow N_1 = N_2$$$

Lean4

theorem fg_of_localized_maximal (N : Submodule R M) (H : ∀ (P : Ideal R) [P.IsMaximal], (N.localized P.primeCompl).FG) :
    N.FG :=
  N.fg_of_isLocalized_maximal _ _ _ H

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