English
The map toFractionRing is equal to the standard algEquiv arising from IsLocalization, i.e., toFractionRing equals IsLocalization.algEquiv on K[X].
Русский
Отображение toFractionRing совпадает с стандартной изоморфизмом IsLocalization, полученным из локализации.
LaTeX
$$$ toFractionRing = IsLocalization.algEquiv (nonZeroDivisors (Polynomial K)) (FractionRing (Polynomial K)) (RatFunc K)$$$
Lean4
@[simp]
theorem ofFractionRing_eq : (ofFractionRing : FractionRing K[X] → RatFunc K) = 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]
