isFractionRing_ofField — Mathlib

English

The subalgebra Localization.subalgebra.ofField K S hS is equipped with IsFractionRing to K, i.e., K is the fraction field of that subalgebra.

Русский

Подалгебре Localization.subalgebra.ofField K S hS сопоставлено IsFractionRing относительно K; то есть K является полем дробей этой подалгебры.

LaTeX

$$$$ \text{IsFractionRing } (\operatorname{ofField} K S hS) \ K $$$$

Lean4

instance isFractionRing_ofField : IsFractionRing (ofField K S hS) K :=
  inferInstance

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