Golfing

Stream: FLT-regular

[Riccardo Brasca]

Currently NormPrime.lean is only used to prove that ζ - 1 is prime. Using current mathlib we can give a better proof (morally is the same one, but it is more natural). Does anyone see a reason to keep it?

[Riccardo Brasca]

Well, almost. @Andrew Yang proof uses exists_int_sModEq, but result can be PRed immediately.

[Riccardo Brasca]

I've PRed the fact that ζ-1 is prime in #8228. I am a little bit sad that it does not hold for the 1-th cyclotomic extension.

[Riccardo Brasca]

(but the ideal generated by ζ-1 is always prime)

[Kevin Buzzard]

We are convinced that 1 is not prime but an argument can be made for 0 being prime: it's pre-prime and not a unit, for example.

[Junyan Xu]

Yeah, currently docs#Ideal.span_singleton_prime requires a side condition p ≠ 0 but docs#Nat.prime_iff doesn't ...