mk_def_of_ne — Mathlib

English

If q ≠ 0, then RatFunc.mk p q equals the localization form with a witness that q is not a zero divisor.

Русский

Если q ≠ 0, RatFunc.mk p q равен форме локализации с подтверждением, что q не является нулевым делителем.

LaTeX

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

Lean4

theorem mk_def_of_ne (p : K[X]) {q : K[X]} (hq : q ≠ 0) :
    RatFunc.mk p q =
      ofFractionRing (IsLocalization.mk' (FractionRing K[X]) p ⟨q, mem_nonZeroDivisors_iff_ne_zero.mpr hq⟩) :=
  mk_def_of_mem p _

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