num_div — Mathlib

English

If q ≠ 0, then the numerator of p/q is

Русский

Если q ≠ 0, то числитель p/q равен

LaTeX

$$$\operatorname{num}\left(\dfrac{p}{q}\right) = C\left(\dfrac{q}{\gcd(p,q)}\right)^{-1} \cdot \left(\dfrac{p}{\gcd(p,q)}\right),\quad q \neq 0$$$

Lean4

@[simp]
theorem num_div (p q : K[X]) :
    num (algebraMap _ _ p / algebraMap _ _ q) = Polynomial.C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q) :=
  by
  by_cases hq : q = 0
  · simp [hq]
  · exact num_div' p hq

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