instDivisionRingNonZeroDivisors — Mathlib

English

The Ore localization at the nonzero divisors yields a division ring.

Русский

Локализация по не нулевым делителям по Оре образует деление кольца (Division Ring).

LaTeX

$$The Ore Localization at nonZeroDivisors(R) is a DivisionRing.$$

Lean4

instance : DivisionRing R[R⁰⁻¹] where
  mul_inv_cancel := OreLocalization.mul_inv_cancel
  inv_zero := OreLocalization.inv_zero
  nnqsmul := _
  nnqsmul_def := fun _ _ => rfl
  qsmul := _
  qsmul_def := fun _ _ => rfl

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