instIsFractionRing — Mathlib

English

If R is a field, then R is the fraction ring of R over itself; i.e., the localization of R by nonZeroDivisors(R) is canonically R.

Русский

Если R — поле, то R является дробной локализацией самого себя; то есть локализация R по множеству ненулевых делителей совпадает с R.

LaTeX

$$$\text{IsFractionRing}(R,R)$ for field R$$

Lean4

instance {R : Type*} [Field R] : IsFractionRing R R :=
  IsLocalization.at_units _ (fun _ ↦ isUnit_of_mem_nonZeroDivisors)

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