Associated (ζₚ - 1)ᵖ⁻¹ p

Stream: Is there code for X?

[Andrew Yang]

Do we know that (ζₚ - 1)ᵖ⁻¹ and p are associates in ℤ[ζₚ]?

[Eric Rodriguez]

It's at least in flt-regular

[Eric Rodriguez]

If its not there explicitly it'll be there as some multiplication

[Andrew Yang]

The closest I could find is docs#IsPrimitiveRoot.sub_one_norm_prime.

[Eric Rodriguez]

hmm, yeah I can't seem to find it. Maybe it's easy to build with flt-reg's is_primitive_root.zeta_pow_sub_eq_unit_zeta_sub_one? (apologies for the lean3 name)

[Riccardo Brasca]

Maybe you can use docs#RingOfIntegers.dvd_norm to get one divisibility, and then docs#RingOfIntegers.isUnit_norm to get that the quotient is a unit.

[Andrew Yang]

I think docs#RingOfIntegers.dvd_norm can only give you ζ - 1 ∣ p?

[Riccardo Brasca]

Ops, yes. Too much teaching today

[Kevin Buzzard]

One approach would be to first prove that $\zeta^i-1$ is an associate of $\zeta-1$ for $0<i<p-1$.

[Kevin Buzzard]

(the proof is that $\zeta-1$ divides $\zeta^{i}-1$ because you can write down the quotient explicitly, but $\zeta-1=\zeta^N-1$ for any $N$ congruent to $1$ mod $p$, and so you can choose $N$ a multiple of $i$ and do the trick the other way around).

And then $\prod_{0<i<p}(\zeta^i-1)$ is $(X^p-1)/(X-1)$ evaluated at $X=1$ which is $p$ modulo a possible sign error.

[Eric Rodriguez]

Kevin Buzzard said:

(the proof is that $\zeta-1$ divides $\zeta^{i}-1$ because you can write down the quotient explicitly, but $\zeta-1=\zeta^N-1$ for any $N$ congruent to $1$ mod $p$, and so you can choose $N$ a multiple of $i$ and do the trick the other way around).

And then $\prod_{0<i<p}(\zeta^i-1)$ is $(X^p-1)/(X-1)$ evaluated at $X=1$ which is $p$ modulo a possible sign error.

is_primitive_root.zeta_pow_sub_eq_unit_zeta_sub_one is this but more general. we should PR it