Zulip Chat Archive

Stream: FLT-regular

Topic: Golfing

Riccardo Brasca (Nov 06 2023 at 15:12):

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 (Nov 06 2023 at 15:33):

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

Riccardo Brasca (Nov 06 2023 at 16:58):

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 (Nov 06 2023 at 16:59):

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

Kevin Buzzard (Nov 06 2023 at 17:11):

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 (Nov 06 2023 at 17:24):

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

Last updated: Dec 20 2023 at 11:08 UTC