algebraMap_liftAlgebra — Mathlib

English

There is an A-algebra isomorphism between FractionRing A and any fraction field K with IsFractionRing A K.

Русский

Существует A-алгебраическое изоморфизм между FractionRing A и любым полем дробей K с IsFractionRing A K.

LaTeX

$$FractionRing.algEquiv (A) (K) [CommRing K] [Algebra A K] [IsFractionRing A K] : FractionRing A ≃_A[A] K$$

Lean4

theorem algebraMap_liftAlgebra :
    have := (FaithfulSMul.algebraMap_injective R K).isDomain
    algebraMap (FractionRing R) K = IsFractionRing.lift (FaithfulSMul.algebraMap_injective R _) :=
  rfl

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