at_units — Mathlib

English

If S is a localization of R at M that sits inside the submonoid of units, then S is indeed a localization of R at S.

Русский

Если S — локализация R в M и подмножество M входит в множество единиц, тогда S является локализацией R при этом образуется локализация в S.

LaTeX

$$$$ \\text{IsLocalization } S R $$$$

Lean4

theorem at_units (S : Submonoid R) (hS : S ≤ IsUnit.submonoid R) : IsLocalization S R
    where
  map_units y := hS y.prop
  surj := fun s ↦ ⟨⟨s, 1⟩, by simp⟩
  exists_of_eq := fun {x y} (e : x = y) ↦ ⟨1, e ▸ rfl⟩

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