mem_freeLocus — Mathlib

English

For any p, membership p ∈ freeLocus R M is equivalent to freeness of the localized module at p.

Русский

Для любого p выполняется эквивалентность: p принадлежит свободному локусу означает, что локализованный модуль свободен.

LaTeX

$$$p \in \mathrm{freeLocus}(R,M) \iff \mathrm{Module.Free}(\mathrm{Localization.AtPrime}(p.asIdeal), \mathrm{LocalizedModule}(p.asIdeal.primeCompl M))$$$

Lean4

theorem mem_freeLocus {p} :
    p ∈ freeLocus R M ↔ Module.Free (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl M) :=
  Iff.rfl

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