instRing — Mathlib

English

If R is a ring and S is an Ore set, then the Ore localization R[S⁻¹] carries a natural ring structure extending that of R.

Русский

Если R — кольцо, и S — множество Оре, то локализация по Оре, R[S⁻¹], получает естественную структуру кольца, продолжающую структуру R.

LaTeX

$$$R[S^{-1}]$ is a ring.$$

Lean4

instance : Ring R[S⁻¹] where
  __ := inferInstanceAs (Semiring R[S⁻¹])
  __ := inferInstanceAs (AddGroup R[S⁻¹])

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