isFractionRing

Mathlib.RingTheory.Localization.AsSubring

URI: https://scilib.ai/kg/mathlib#Localization.subalgebra.isFractionRing

English

The subalgebra Localization.subalgebra K S hS forms a fraction ring of K, i.e., is itself a fraction ring over K.

Русский

Подалгебра Localization.subalgebra K S hS образует дробное кольцо над K.

LaTeX

$$$IsFractionRing\\ (subalgebra K S hS)\\ K$$$

Lean4

instance isFractionRing : IsFractionRing (subalgebra K S hS) K :=
  IsFractionRing.isFractionRing_of_isLocalization S _ _ hS

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru