denom_div — Mathlib

English

For p, q ∈ K[X] with q ≠ 0, the denominator of p/q is

Русский

Для p, q ∈ K[X], q ≠ 0, знаменатель p/q равен

LaTeX

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

Lean4

@[simp]
theorem denom_div (p : K[X]) {q : K[X]} (hq : q ≠ 0) :
    denom (algebraMap _ _ p / algebraMap _ _ q) = Polynomial.C (q / gcd p q).leadingCoeff⁻¹ * (q / gcd p q) := by
  rw [denom, numDenom_div _ hq]

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