isFractionRing_range_mapToFractionRing

English

The range of mapToFractionRing carries a fraction field structure over K.

Русский

Диапазон mapToFractionRing имеет структуру дробного поля над K.

LaTeX

$$$IsFractionRing\\ (\\mathrm{mapToFractionRing}\\ K S B hS).range\\ K$$$

Lean4

instance isFractionRing_range_mapToFractionRing (B : Type*) [CommRing B] [Algebra A B] [IsLocalization S B]
    (hS : S ≤ A⁰) : IsFractionRing (mapToFractionRing K S B hS).range K :=
  IsFractionRing.isFractionRing_of_isLocalization S _ _ hS

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