English
There is a canonical isomorphism of rings between RatFunc(K) and the field of fractions of the polynomial ring K[X], i.e. RatFunc(K) ≅ FractionRing(K[X]).
Русский
Существует каноническое изоморождение колец между RatFunc(K) и полем дробей (полиномов) K[X], то есть RatFunc(K) ≅ FractionRing(K[X]).
LaTeX
$$$\mathrm{RatFunc}(K) \cong \mathrm{FractionRing}(K[X])$$$
Lean4
/-- `RatFunc K` is isomorphic to the field of fractions of `K[X]`, as rings.
This is an auxiliary definition; `simp`-normal form is `IsLocalization.algEquiv`.
-/
@[simps apply]
def toFractionRingRingEquiv : RatFunc K ≃+* FractionRing K[X]
where
toFun := toFractionRing
invFun := ofFractionRing
map_add' := fun ⟨_⟩ ⟨_⟩ => by simp [← ofFractionRing_add]
map_mul' := fun ⟨_⟩ ⟨_⟩ => by simp [← ofFractionRing_mul]
