Weierstrass polynomials over a commutative ring

Lemmas about polynomials over an arbitrary commutative ring that do not depend on the coefficient field: the Weierstrass polynomial with zero coefficients is X^d, the one of degree 0 is 1, a monic polynomial is the Weierstrass polynomial of its own coefficients, and a monic polynomial of degree 0 is 1.

Weierstrass polynomials over a commutative ring

theorem Analytic.weierstrassPolynomial_zero {R : Type u_1} [CommRing R] (d : ℕ) : (weierstrassPolynomial d fun (x : Fin d) => 0) = Polynomial.X ^ d

The Weierstrass polynomial with zero coefficients is X^d.

theorem Analytic.weierstrassPolynomial_zero_eq_one {R : Type u_1} [CommRing R] (c : Fin 0 → R) : weierstrassPolynomial 0 c = 1

weierstrassPolynomial 0 c = 1.

theorem Analytic.eq_weierstrassPolynomial_coeff_of_monic {R : Type u_1} [CommRing R] {Q : Polynomial R} (hQ : Q.Monic) : Q = weierstrassPolynomial Q.natDegree fun (j : Fin Q.natDegree) => Q.coeff (Q.natDegree - 1 - ↑j)

A monic polynomial is the Weierstrass polynomial of its own coefficients.

Monic polynomials of degree zero

theorem Analytic.eq_one_of_monic_natDegree_eq_zero {R : Type u_1} [CommRing R] {p : Polynomial R} (hp : p.Monic) (h0 : p.natDegree = 0) : p = 1

A monic polynomial of degree 0 is 1.