instLocalization — Mathlib

English

The localization at S inherits Artinian property, i.e., IsArtinianRing (Localization S).

Русский

Локализация по S наследует свойство Артиниана: IsArtinianRing (Localization S).

LaTeX

$$$IsArtinianRing\ (Localization\ S)$$$

Lean4

/-- `IsArtinianRing.localization_artinian` can't be made an instance, as it would make `S` + `R`
into metavariables. However, this is safe. -/
instance : IsArtinianRing (Localization S) :=
  localization_artinian S _

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