isLocalization_ofField — Mathlib

English

Let S be a subalgebra of K (via Localization.subalgebra.ofField). Then S has K as its field of fractions; i.e., IsFractionRing S K holds.

Русский

Пусть S — подалгебра K (через Localization.subalgebra.ofField). Тогда у S полем дробей является K; то есть IsFractionRing S K выполняется.

LaTeX

$$$$ \text{IsFractionRing } \big(\operatorname{Localization.subalgebra.ofField} K S hS\big) \, K $$$$

Lean4

instance isLocalization_ofField : IsLocalization S (ofField K S hS) :=
  by
  rw [ofField_eq]
  exact isLocalization_subalgebra K S hS

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