mk_eq_div — Mathlib

English

For polynomials p,q ∈ K[X], RatFunc.mk p q equals algebraMap p divided by algebraMap q in RatFunc K.

Русский

Для многочленов p,q ∈ K[X], RatFunc.mk p q равен algebraMap p делённому на algebraMap q в RatFunc K.

LaTeX

$$$\\operatorname{RatFunc}.mk\\,p\\,q = \\frac{\\text{algebraMap } p}{\\text{algebraMap } q}$$$

Lean4

@[simp]
theorem mk_eq_div (p q : K[X]) : RatFunc.mk p q = algebraMap _ _ p / algebraMap _ _ q := by
  simp only [mk_eq_div', ofFractionRing_div, ofFractionRing_algebraMap]

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