mk_coe_def — Mathlib

English

RatFunc.mk p q equals the isLocalization form via.mk', i.e. RatFunc.mk p q = ofFractionRing(IsLocalization.mk' _ p q).

Русский

RatFunc.mk p q эквивалентен форме локализации через mk'.

LaTeX

$$$\\text{RatFunc.mk}\\, p\\, q = \\text{ofFractionRing}(\\text{IsLocalization.mk'}\\, p\, q)$$$

Lean4

theorem mk_coe_def (p : K[X]) (q : K[X]⁰) : RatFunc.mk p q = ofFractionRing (IsLocalization.mk' _ p q) := by
  simp only [mk_eq_div', ← Localization.mk_eq_mk', FractionRing.mk_eq_div]

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