theorem Hex.DensePoly.size_scale_field {F : Type u} [Lean.Grind.Field F] [DecidableEq F] {a : F} (ha : a ≠ 0) (p : DensePoly F) : (scale a p).size = p.size

Scaling a polynomial by a nonzero field element preserves its stored size.

theorem Hex.DensePoly.monic_monicize {F : Type u} [Lean.Grind.Field F] [DecidableEq F] {p : DensePoly F} (hp : p ≠ 0) : p.monicize.Monic

Compatibility name for the monicity theorem used by Smith clients.

theorem Hex.DensePoly.scale_inv_eq_monicize {F : Type u} [Lean.Grind.Field F] [DecidableEq F] {p : DensePoly F} (hp : p ≠ 0) : scale p.leadingCoeff⁻¹ p = p.monicize

The nonzero branch of monic normalization, exposed for algebraic clients.

theorem Hex.DensePoly.dvd_monicize {F : Type u} [Lean.Grind.Field F] [DecidableEq F] (p : DensePoly F) : p ∣ p.monicize

Every polynomial divides its monic associate.

theorem Hex.DensePoly.eq_C_leadingCoeff_of_size_one {F : Type u} [Lean.Grind.Field F] [DecidableEq F] {p : DensePoly F} (hp : p.size = 1) : p = C p.leadingCoeff

A size-one polynomial is the constant polynomial of its leading coefficient.