Denominators of rational polynomials

DefinitionDenominator of a rational polynomial#✓fully proved

For a polynomial \(P \in \mathbb{Q}[x]\), the denominator \(\operatorname{denom}(P)\) is the least common multiple of the denominators (in lowest terms) of the nonzero coefficients of \(P\); in particular \(\operatorname{denom}(0) = 1\). Thus \(\operatorname{denom}(P) = 1\) exactly when \(P \in \mathbb{Z}[x]\).

public def polynomialDenominator (P : ℚ[X]) : ℕ :=
  P.support.lcm fun i => (P.coeff i).den
Sources
  • Bernd C. Kellner, On the Finiteness of Bernoulli Polynomials Whose Derivative Has Only Integral Coefficients, Journal of Integer Sequences 27 (2024), Article 24.2.8, Section 2 (notation denom).
Used by 9
Used byCoefficient denominators divide the denominator of a polynomial · Denominator one characterizes integer polynomials · Integrality of the derivative of a Bernoulli polynomial · Product formula for the denominator of \(B_n(x) - B_n\) · Denominators of higher derivatives of Bernoulli polynomials · Indices of Bernoulli polynomials with integral \(k\)-th derivative · Denominators of Bernoulli polynomials are even · The derivative of \(B_1(x)\) has integer coefficients · The Bernoulli polynomial \(B_0(x)\) has denominator one

TheoremCoefficient denominators divide the denominator of a polynomial#✓fully proved

For every polynomial \(P \in \mathbb{Q}[x]\) and every \(i \in \mathbb{N}\), the denominator (in lowest terms) of the coefficient of \(x^i\) in \(P\) divides the denominator \(\operatorname{denom}(P)\) of \(P\).

public theorem coeff_den_dvd_polynomialDenominator (P : ℚ[X]) (i : ℕ) :
    (P.coeff i).den ∣ polynomialDenominator P
Sources
  • Bernd C. Kellner, On the Finiteness of Bernoulli Polynomials Whose Derivative Has Only Integral Coefficients, Journal of Integer Sequences 27 (2024), Article 24.2.8, Section 2 (definition of denom).
Uses 1 · Used by 1
Statement usesDenominator of a rational polynomial
Used byDenominator one characterizes integer polynomials

TheoremDenominator one characterizes integer polynomials#✓fully proved

For every polynomial \(P \in \mathbb{Q}[x]\), its denominator \(\operatorname{denom}(P)\) equals \(1\) if and only if, for every \(i \in \mathbb{N}\), the coefficient of \(x^i\) in \(P\) is an integer.

public theorem polynomialDenominator_eq_one_iff (P : ℚ[X]) :
    polynomialDenominator P = 1 ↔ ∀ i, (P.coeff i).den = 1
Sources
  • Bernd C. Kellner, On the Finiteness of Bernoulli Polynomials Whose Derivative Has Only Integral Coefficients, Journal of Integer Sequences 27 (2024), Article 24.2.8, Section 1 (denom(B_n(x)) > 1 is equivalent to B_n(x) ∉ ℤ[x]).
Uses 2 · Used by 2
Statement usesDenominator of a rational polynomial
Proof usesCoefficient denominators divide the denominator of a polynomial
Used byThe derivative of \(B_1(x)\) has integer coefficients · The Bernoulli polynomial \(B_0(x)\) has denominator one
3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.