ofFractionRing_mk' — Mathlib

English

The fraction ring embedding of x and y yields the same localization as the direct mkp', i.e., ofFractionRing (IsLocalization.mk' _ x y) = IsLocalization.mk' (RatFunc K) x y.

Русский

Образ дробного кольца x/y через mk' совпадает с прямым mk' в RatFunc K.

LaTeX

$$$ ofFractionRing (IsLocalization.mk' _ x y) = IsLocalization.mk' (RatFunc K) x y$$$

Lean4

theorem ofFractionRing_mk' (x : K[X]) (y : K[X]⁰) :
    ofFractionRing (IsLocalization.mk' _ x y) = IsLocalization.mk' (RatFunc K) x y := by
  rw [IsFractionRing.mk'_eq_div, IsFractionRing.mk'_eq_div, ← mk_eq_div', ← mk_eq_div]

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