mk_eq_div' — Mathlib

English

For polynomials p,q with q ≠ 0, RatFunc.mk p q equals the image of p/q in the fraction field: ofFractionRing(algebraic quotient).

Русский

Для полиномов p,q с q ≠ 0 RatFunc.mk p q совпадает с образом дроби p/q в дробной области.

LaTeX

$$$\\text{RatFunc.mk}\\, p\\, q = \\text{ofFractionRing}(\\text{algebraMap}(p)/\\text{algebraMap}(q))$$$

Lean4

theorem mk_eq_div' (p q : K[X]) : RatFunc.mk p q = ofFractionRing (algebraMap _ _ p / algebraMap _ _ q) := by
  rw [RatFunc.mk]

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