localization_unit_isIso' — Mathlib

English

For any ring R, the unit map to Localization Away(1) is an isomorphism; this holds in the base type as an instance.

Русский

Для любого кольца R единичное отображение в Localization Away(1) является изоморфизмом.

LaTeX

$$$\mathrm{IsIso}\big(\text{CommRingCat.ofHom }(\text{algebraMap } R (\mathrm{Localization Away}(1)))\big)$$$

Lean4

instance localization_unit_isIso' (R : CommRingCat) :
    @IsIso CommRingCat _ R _ (CommRingCat.ofHom <| algebraMap R (Localization.Away (1 : R))) :=
  by
  cases R
  exact localization_unit_isIso _

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