English
For any x ∈ RatFunc K, numDenom(x) returns a pair of polynomials (numerator, denominator) with the denominator monic, obtained by a canonical lift.
Русский
Для любого x ∈ RatFunc K функция numDenom(x) возвращает пару многочленов (числитель, знаменатель) с знаменателем нормированным до моного, полученную каноническим способом.
LaTeX
$$$\operatorname{numDenom}(x) = (p, q) \quad\text{with } q \text{ monic and } x= p/q$$$
Lean4
/-- `RatFunc.numDenom` are numerator and denominator of a rational function over a field,
normalized such that the denominator is monic. -/
def numDenom (x : RatFunc K) : K[X] × K[X] :=
x.liftOn'
(fun p q =>
if q = 0 then ⟨0, 1⟩
else
let r := gcd p q
⟨Polynomial.C (q / r).leadingCoeff⁻¹ * (p / r), Polynomial.C (q / r).leadingCoeff⁻¹ * (q / r)⟩)
(by
intro p q a hq ha
dsimp
rw [if_neg hq, if_neg (mul_ne_zero ha hq)]
have ha' : a.leadingCoeff ≠ 0 := Polynomial.leadingCoeff_ne_zero.mpr ha
have hainv : a.leadingCoeff⁻¹ ≠ 0 := inv_ne_zero ha'
simp only [Prod.ext_iff, gcd_mul_left, normalize_apply a, Polynomial.coe_normUnit, mul_assoc,
CommGroupWithZero.coe_normUnit _ ha']
have hdeg : (gcd p q).degree ≤ q.degree := degree_gcd_le_right _ hq
have hdeg' : (Polynomial.C a.leadingCoeff⁻¹ * gcd p q).degree ≤ q.degree :=
by
rw [Polynomial.degree_mul, Polynomial.degree_C hainv, zero_add]
exact hdeg
have hdivp : Polynomial.C a.leadingCoeff⁻¹ * gcd p q ∣ p := (C_mul_dvd hainv).mpr (gcd_dvd_left p q)
have hdivq : Polynomial.C a.leadingCoeff⁻¹ * gcd p q ∣ q := (C_mul_dvd hainv).mpr (gcd_dvd_right p q)
rw [EuclideanDomain.mul_div_mul_cancel ha hdivp, EuclideanDomain.mul_div_mul_cancel ha hdivq,
leadingCoeff_div hdeg, leadingCoeff_div hdeg', Polynomial.leadingCoeff_mul, Polynomial.leadingCoeff_C,
div_C_mul, div_C_mul, ← mul_assoc, ← Polynomial.C_mul, ← mul_assoc, ← Polynomial.C_mul]
constructor <;> congr <;>
rw [inv_div, mul_comm, mul_div_assoc, ← mul_assoc, inv_inv, mul_inv_cancel₀ ha', one_mul, inv_div])
