English
Let p, q be polynomials in K[x] with q ≠ 0. In the rational function p/q, the numerator and denominator are explicitly given by the gcd-reduced form: if g = gcd(p, q), then
Русский
Пусть p, q — многочлены над полем K с q ≠ 0. В рациональной функции p/q числитель и знаменатель выражаются через НОД: если g = gcd(p, q), то
LaTeX
$$$\operatorname{numDenom}\left(\dfrac{p}{q}\right) = \left( C\left(\dfrac{q}{\gcd(p,q)}\right)^{-1} \cdot \dfrac{p}{\gcd(p,q)},\; C\left(\dfrac{q}{\gcd(p,q)}\right)^{-1} \cdot \dfrac{q}{\gcd(p,q)} \right)$$$
Lean4
@[simp]
theorem numDenom_div (p : K[X]) {q : K[X]} (hq : q ≠ 0) :
numDenom (algebraMap _ _ p / algebraMap _ _ q) =
(Polynomial.C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q),
Polynomial.C (q / gcd p q).leadingCoeff⁻¹ * (q / gcd p q)) :=
by
rw [numDenom, liftOn'_div, if_neg hq]
intro p
rw [if_pos rfl, if_neg (one_ne_zero' K[X])]
simp
