Case II

Stream: FLT-regular

[Riccardo Brasca]

I will be a little busy in the next few weeks, but we can start thinking about a strategy (but don't forget to open PRs about what we've already done if you have time!).

It seems we agree it's better to postpone the proof of Kummer's lemma to a later moment, so we can prove it for primes that (are regular and) satisfy it.

I've been reading Conrad's notes. They're quite elementary, but also with a lot of calculations (with congruences modulo $1-\zeta$ and $(1-\zeta)^2$ and similar things). I guess all these calculations are in principle possible, but I don't know if it is the right thing to do.

What do you think?

[Chris Birkbeck]

I agree, from the profs I've seen this seems the most reasonable. Ill try to finish going over the proof and making into a blueprint

[Riccardo Brasca]

I will be a little busy in the next few weeks, but we can start thinking about a strategy (but don't forget to open PRs about what we've already done if you have time!).

It seems we agree it's better to postpone the proof of Kummer's lemma to a later moment, so we can prove it for primes that (are regular and) satisfy it.

I've been reading Conrad's notes. They're quite elementary, but also with a lot of calculations (with congruences modulo $1-\zeta$ and $(1-\zeta)^2$ and similar things). I guess all these calculations are in principle possible, but I don't know if it is the right thing to do.

What do you think?

[Chris Birkbeck]

I agree, from the profs I've seen this seems the most reasonable. Ill try to finish going over the proof and making into a blueprint

[Andrew Yang]

I might have accidentally finished case II except Kummer's lemma.

[Alex J. Best]

What a happy accident, congratulations!

[Alex J. Best]

We should definitely just merge this andmake the Lean 4 version the master branch now :smile:

[Johan Commelin]

An accident of > 1000 lines :rofl:

[Riccardo Brasca]

That's wonderful news!!

[Riccardo Brasca]

I think we should restart the PR process

[Riccardo Brasca]

I merged @Andrew Yang 's work (thanks again).

[Riccardo Brasca]

It's time to start thinking about Kummer's lemma...

[Chris Birkbeck]

Yeah! I saw someone made a lean4 blueprint. Maybe we can start mapping that out

[Riccardo Brasca]

Yes, it's a good idea. We need to think about the math... maybe the approach with L-functions is a good one

[Riccardo Brasca]

I think it would be really nice to have the connections with Bernoulli numbers, since it is very easy to check in practice

[Chris Birkbeck]

Yes it would be nice to have more examples of regular primes :)

[Chris Birkbeck]

From memory the borevich-shafarevich proof seemed the most accessible, but Washington's book has a some different ones which might be worth looking at.

[Chris Birkbeck]

I mean proof in borevich-shafarevich's book

[Ruben Van de Velde]

I PRd a few of the preliminaries for case II at https://github.com/leanprover-community/mathlib4/pull/7453

[Ruben Van de Velde]

Will push a bump in a bit

[Riccardo Brasca]

Speaking of bumps, I bumbed mathlib yesterday, and there is now a new timeout. It's a little bit sad that things get worst...

[Ruben Van de Velde]

-set_option maxHeartbeats 800000
 lemma fltIdeals_coprime2_lemma [Fact (p : ℕ).Prime] (ph : 5 ≤ p) {x y : ℤ} {η₁ η₂ : R}
     (hη₁ : η₁ ∈ nthRootsFinset p R)
     (hη₂ : η₂ ∈ nthRootsFinset p R) (hdiff : η₁ ≠ η₂) (hp : IsCoprime x y)
     (hp2 : ¬(p : ℤ) ∣ (x + y : ℤ)) (hwlog : η₁ ≠ 1) :
     (fltIdeals p x y hη₁) ⊔ (fltIdeals p x y hη₂) = ⊤ := by
-  by_contra h
+  apply by_contradiction
+  intro h

[Eric Rodriguez]

does by_contra still look for decidability?

[Ruben Van de Velde]

That was my guess, but I didn't verify

[Riccardo Brasca]

We should add this to the doc of by_contra

[Ruben Van de Velde]

I started moving a few more at https://github.com/leanprover-community/mathlib4/pull/new/flt-regular ; wip