instIsReducedLocalization — Mathlib

English

There is a generic instance ensuring localization preserves reducedness for any submonoid M.

Русский

Существует универсальная инстанция, сохраняющая редуцированность локализацией для любого подмоноида M.

LaTeX

$$$\\text{instance } IsReduced( Localization(M) )$$$

Lean4

instance {R : Type*} [CommRing R] (M : Submonoid R) [IsReduced R] : IsReduced (Localization M) :=
  isReduced_localizationPreserves M _ inferInstance

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