toFractionRing_eq — Mathlib

English

The toFractionRing map is equal to the algebra isomorphism IsLocalization.algEquiv between K[X]⁰ and RatFunc K.

Русский

Отображение toFractionRing равняется изоморфизму алгебры IsLocalization.algEquiv между K[X]⁰ и RatFunc K.

LaTeX

$$$ toFractionRing = IsLocalization.algEquiv K[X]⁰ _ _ $$$

Lean4

@[simp]
theorem toFractionRing_eq : (toFractionRing : RatFunc K → FractionRing K[X]) = IsLocalization.algEquiv K[X]⁰ _ _ :=
  funext fun ⟨x⟩ =>
    Localization.induction_on x fun x => by
      simp only [Localization.mk_eq_mk'_apply, ofFractionRing_mk', IsLocalization.algEquiv_apply,
        IsLocalization.map_mk', RingHom.id_apply]

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