Minimal polynomial of `ζ - 1`

Stream: Is there code for X?

[Riccardo Brasca]

Let p : ℕ be a prime and let ζ : ℂ by a primitive p-th root of unity. Mathlib knows that the minimal polynomial, over ℤ, of ζ is cyclotomic p ℤ = geom_sum X p. I need to know that the minimal polynomial of ζ - 1 is Eisenstein at p. Mathematically this is $\Phi_p(x + 1)$ and a simple calculation shows it is Eiseinstein.

I am not sure about how to prove this in mathlib. Should I use docs#polynomial.comp? The API seems a quite small, for example I don't find that the composition of monic polynomials is monic (this is needed to show that (cyclotomic p ℤ).comp (X+1) is the minimal polynomial of ζ - 1. Is there a better way?

[Riccardo Brasca]

Ah, in data.polynomial.ring_division the API is more complete