subsingleton — Mathlib

English

If S contains zero, then the localization at S is a singleton; i.e., LocalizationMap is subsingleton.

Русский

Если 0 ∈ S, локализация по S является синглетной, то есть локализационная карта относится к единственному элементу.

LaTeX

$$$\\text{LocalizationMap.subsingleton}(S,N,f) \\Rightarrow \\text{Subsingleton}(N)$$$

Lean4

/-- If `S` contains `0` then the localization at `S` is trivial. -/
theorem subsingleton (f : LocalizationMap S N) (h : 0 ∈ S) : Subsingleton N :=
  by
  refine ⟨fun a b ↦ ?_⟩
  rw [← LocalizationMap.mk'_sec f a, ← LocalizationMap.mk'_sec f b, LocalizationMap.eq]
  exact ⟨⟨0, h⟩, by simp only [zero_mul]⟩

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