mk_eq_localization_mk — Mathlib

English

For p ∈ K[X] and q ≠ 0, RatFunc.mk p q equals the localized form Localization.mk p ⟨q, mem...⟩.

Русский

Для p ∈ K[X] и q ≠ 0 RatFunc.mk p q равен локализованной форме Localization.mk p ⟨q, …⟩.

LaTeX

$$$\\text{RatFunc.mk}\\, p\\, q = \\text{ofFractionRing}(\\text{Localization.mk} \\, p \\langle q, \\text{mem_nonZeroDivisors_iff_ne_zero.mpr hq}\\rangle)$$$

Lean4

theorem mk_eq_localization_mk (p : K[X]) {q : K[X]} (hq : q ≠ 0) :
    RatFunc.mk p q = ofFractionRing (Localization.mk p ⟨q, mem_nonZeroDivisors_iff_ne_zero.mpr hq⟩) := by
  rw [mk_def_of_ne _ hq, Localization.mk_eq_mk']

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