## Stream: FLT-regular

### Topic: Case II

#### Riccardo Brasca (Oct 17 2022 at 16:37):

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 (Oct 17 2022 at 17:08):

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 (Oct 17 2022 at 16:37):

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 (Oct 17 2022 at 17:08):

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 (Sep 30 2023 at 15:31):

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

#### Alex J. Best (Sep 30 2023 at 15:54):

What a happy accident, congratulations!

#### Alex J. Best (Sep 30 2023 at 15:55):

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

#### Johan Commelin (Sep 30 2023 at 16:01):

An accident of > 1000 lines :rofl:

#### Riccardo Brasca (Sep 30 2023 at 16:45):

That's wonderful news!!

#### Riccardo Brasca (Sep 30 2023 at 16:46):

I think we should restart the PR process

#### Riccardo Brasca (Oct 01 2023 at 09:44):

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

#### Riccardo Brasca (Oct 01 2023 at 09:44):

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

#### Chris Birkbeck (Oct 01 2023 at 09:45):

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

#### Riccardo Brasca (Oct 01 2023 at 09:55):

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 (Oct 01 2023 at 09:55):

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 (Oct 01 2023 at 09:56):

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

#### Chris Birkbeck (Oct 01 2023 at 09:57):

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 (Oct 01 2023 at 09:58):

I mean proof in borevich-shafarevich's book

#### Ruben Van de Velde (Oct 01 2023 at 23:09):

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

#### Ruben Van de Velde (Oct 02 2023 at 08:16):

Will push a bump in a bit

#### Riccardo Brasca (Oct 02 2023 at 08:32):

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 (Oct 02 2023 at 09:17):

-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
+  intro h


#### Eric Rodriguez (Oct 02 2023 at 09:55):

does by_contra still look for decidability?

#### Ruben Van de Velde (Oct 02 2023 at 09:57):

That was my guess, but I didn't verify

#### Riccardo Brasca (Oct 02 2023 at 10:31):

We should add this to the doc of by_contra

#### Ruben Van de Velde (Oct 02 2023 at 10:42):

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

Last updated: Dec 20 2023 at 11:08 UTC