English
RatFunc K is the fraction field of Polynomial K, i.e., K[X] and RatFunc K form a fraction ring pair.
Русский
RatFunc K является полем дробей над Polynomial K, то есть K[X] и RatFunc K образуют пару полей дробей.
LaTeX
$$$\text{IsFractionRing } K[X] (\text{RatFunc } K)$$$
Lean4
/-- `RatFunc K` is the field of fractions of the polynomials over `K`. -/
instance : IsFractionRing K[X] (RatFunc K)
where
map_units
y := by
rw [← ofFractionRing_algebraMap]
exact (toFractionRingRingEquiv K).symm.toRingHom.isUnit_map (IsLocalization.map_units _ y)
exists_of_eq
{x y} := by
rw [← ofFractionRing_algebraMap, ← ofFractionRing_algebraMap]
exact fun h ↦ IsLocalization.exists_of_eq ((toFractionRingRingEquiv K).symm.injective h)
surj := by
rintro ⟨z⟩
convert IsLocalization.surj K[X]⁰ z
simp only [← ofFractionRing_algebraMap, ← ofFractionRing_mul, ofFractionRing.injEq]
