instFaithfulSMul

Mathlib.RingTheory.Localization.FractionRing

URI: https://scilib.ai/kg/mathlib#IsFractionRing.instFaithfulSMul

English

The R-action on K is faithful whenever the fraction field embedding is injective.

Русский

Действие R на K сохраняет однозначность, когда встраивание инъективно.

LaTeX

$$instance (priority := 100) : FaithfulSMul R K$$

Lean4

instance (priority := 100) : FaithfulSMul R K :=
  (faithfulSMul_iff_algebraMap_injective R K).mpr <| IsFractionRing.injective R K

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

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

Разделы

Аффилиация

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