of_field_isFractionRing — Mathlib

English

A faithful scalar action on K induces a faithful action on the fraction ring.

Русский

Точечное действие скаляров на поле K индуцирует корректное действие на дробную кольцо.

LaTeX

$$FaithfulSMul.of_field_isFractionRing R K$$

Lean4

theorem of_field_isFractionRing (K L : Type*) [Field K] [Semiring L] [Nontrivial L] [Algebra R K] [IsFractionRing R K]
    [Algebra S L] [Algebra K L] [Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L] : FaithfulSMul R S :=
  (faithfulSMul_iff_algebraMap_injective R S).mpr <| algebraMap_injective_of_field_isFractionRing R S K L

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