English
There is an algebra equivalence between RatFunc K and the fraction ring of polynomials, preserving the algebra structure and commuting with algebra maps.
Русский
Существует алгебраическое эквивалентное отображение между RatFunc K и полем частных дробей от полиномов, сохраняющее структуру алгебры и совместимое с алгебраическими отображениями.
LaTeX
$$$\\text{RatFunc } K \\simeq_{\\text{alg}} \\text{FractionRing } \\bigl( \\text{Polynomial } K \\bigr)$$$
Lean4
/-- The equivalence between `RatFunc K` and the field of fractions of `K[X]`
-/
@[simps! apply]
def toFractionRingAlgEquiv (R : Type*) [CommSemiring R] [Algebra R K[X]] : RatFunc K ≃ₐ[R] FractionRing K[X]
where
__ := RatFunc.toFractionRingRingEquiv K
commutes'
r := by
change (RatFunc.mk (algebraMap R K[X] r) 1).toFractionRing = _
rw [mk_one']; rfl
