uniqueOfZeroMem — Mathlib

English

Localizing at a submonoid containing 0 yields the unique (zero) ring.

Русский

Локализация в случае 0 из множества порождает единично-нулевое кольцо.

LaTeX

$$If 0 ∈ M, then S is the unique ring (i.e., the zero ring).$$

Lean4

/-- Localizing at a submonoid with 0 inside it leads to the trivial ring. -/
def uniqueOfZeroMem (h : (0 : R) ∈ M) : Unique S :=
  uniqueOfZeroEqOne <| by simpa using IsLocalization.map_units S ⟨0, h⟩

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