instFieldNonZeroDivisors

Mathlib.RingTheory.OreLocalization.Ring

URI: https://scilib.ai/kg/mathlib#OreLocalization.instFieldNonZeroDivisors

English

Under the hypotheses, the Ore localization at nonZeroDivisors becomes a field.

Русский

При данных гипотезах локализация по не нулевым делителям становится полем.

LaTeX

$$Field (OreLocalization (nonZeroDivisors(R)) R).$$

Lean4

noncomputable instance : Field R[R⁰⁻¹]
    where
  __ := inferInstanceAs (DivisionRing R[R⁰⁻¹])
  __ := inferInstanceAs (CommMonoid R[R⁰⁻¹])

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru