subsingleton_iff — Mathlib

English

If R is a commutative ring and M is Subsingleton, then the localized module LocalizedModule S M is also Subsingleton.

Русский

Если R — коммутативное кольцо и M — субодиночный модуль, то локализованный модуль LocalizedModule S M также субодиночен.

LaTeX

$$$\text{Subsingleton}(M) \Rightarrow \text{Subsingleton}(\mathrm{LocalizedModule}\;S\;M)$$$

Lean4

theorem subsingleton_iff {S : Submonoid R} : Subsingleton (LocalizedModule S M) ↔ ∀ m : M, ∃ r ∈ S, r • m = 0 :=
  IsLocalizedModule.subsingleton_iff S (LocalizedModule.mkLinearMap S M)

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