A divisor of the highest possible degree, and primitive polynomial comparisons

A polynomial divisible by a polynomial of at least its degree is the latter times a constant, and the constant is a unit when the multiple is primitive (Polynomial.IsPrimitive.exists_eq_mul_C_unit_of_dvd_of_natDegree_le). Reversal permutes the coefficients and hence preserves primitivity. Together these facts compare primitive defining polynomials after inversion of a root.

@[simp]

theorem Polynomial.isPrimitive_reverse_iff {R : Type u_1} [CommSemiring R] (p : Polynomial R) : p.reverse.IsPrimitive ↔ p.IsPrimitive

Reversal preserves primitivity, including for polynomials with zero constant term.

theorem Polynomial.exists_eq_mul_C_of_dvd_of_natDegree_le {R : Type u_1} [CommSemiring R] [NoZeroDivisors R] {p q : Polynomial R} (hdvd : q ∣ p) (hdeg : p.natDegree ≤ q.natDegree) : ∃ (c : R), p = q * C c ∧ p.leadingCoeff = q.leadingCoeff * c

A divisor of the highest possible degree is a constant multiple. If q ∣ p and p has degree at most that of q, then p = q * C c for the constant term c of the quotient, and the leading coefficient of p is that of q times c. With p primitive in addition, c is a unit (Polynomial.IsPrimitive.exists_eq_mul_C_unit_of_dvd_of_natDegree_le).

theorem Polynomial.IsPrimitive.exists_eq_mul_C_unit_of_dvd_of_natDegree_le {R : Type u_1} [CommSemiring R] [NoZeroDivisors R] {p q : Polynomial R} (hp : p.IsPrimitive) (hdvd : q ∣ p) (hdeg : p.natDegree ≤ q.natDegree) : ∃ (u : Rˣ), p = q * C ↑u

A primitive polynomial divisible by a polynomial of at least its degree is the latter times a constant unit.