toFractionRingRingEquiv_symm_eq — Mathlib

English

The symmetric of the fraction ring ring equivalence coincides with the algebra equivalence on RatFunc, i.e., (toFractionRingRingEquiv K).symm equals IsLocalization.algEquiv’s toRingEquiv.

Русский

Симметрическое отображение круговой эквивалентности дробного кольца совпадает с алгебраической эквивалентностью RatFunc.

LaTeX

$$$(\text{toFractionRingRingEquiv } K).\text{symm} = (\text{IsLocalization.algEquiv } K[X]⁰ _ _).toRingEquiv$$$

Lean4

@[simp]
theorem toFractionRingRingEquiv_symm_eq :
    (toFractionRingRingEquiv K).symm = (IsLocalization.algEquiv K[X]⁰ _ _).toRingEquiv :=
  by
  ext x
  simp [toFractionRingRingEquiv, ofFractionRing_eq]

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