mathlib4 feat (Mathlib.NumberTheory.Cyclotomic.Three): new file

We add a new file Mathlib.NumberTheory.Cyclotomic.Three containing various results about the third cyclotomic field.

In particular we give a a completely explicit description of the group of units and we prove eq_one_or_neg_one_of_unit_of_congruent: Kummer's lemma in the case p=3.

From the flt3 project at LFTCM2024.

May 08 '24 15:05 riccardobrasca

You can change lines by 436-446 with

replace hdim : 1 < pB.dim := by
    rw [Nat.one_lt_iff_ne_zero_and_ne_one, hdim]
    refine ⟨by simp only [ne_eq, mul_eq_zero, pow_eq_zero_iff', PNat.ne_zero, false_and, false_or,
      Nat.sub_eq_zero_iff_le, not_le, Nat.Prime.one_lt hp.out], ne_of_gt ?_⟩
    by_cases hk : k = 0
    · simp_all [hk, zero_add, pow_one, pow_zero, one_mul, Nat.lt_sub_iff_add_lt, Nat.reduceAdd];
        assumption
    · exact one_lt_mul_of_lt_of_le (one_lt_pow hp.1.one_lt hk)
        (have := Nat.Prime.two_le hp.out; by omega)

(not a big improvement, but probably an easier proof). For some reason, I could not comment this directly in the file.

May 24 '24 16:05 faenuccio

Also, you can replace the proof of not_exists_int_prime_dvd_sub_of_prime_ne_two by

  refine not_exists_int_prime_dvd_sub_of_prime_pow_ne_two hζ (fun h ↦ ?_)
  simp_all only [(@Nat.Prime.pow_eq_iff 2 p (k+1) Nat.prime_two).mp (by assumption_mod_cast),
    pow_one, ne_eq]

May 24 '24 16:05 faenuccio

@MichaelStollBayreuth I am confused by all your comments (but thanks for the review!), applying them gives errors, that I can fix of course, but I guess I will write again my own proof. It seems to me there are two things:

using fin_cases: I agree it should work, but it doesn't in the various experiments I tried.
using a list instead of a finset: this is easy to implement, but as you said is further from the informal statement and I don't see any advantage (but I am happy to change my mind).

May 28 '24 19:05 riccardobrasca

@MichaelStollBayreuth I am confused by all your comments (but thanks for the review!), applying them gives errors, that I can fix of course, but I guess I will write again my own proof. It seems to me there are two things:
* using `fin_cases`: I agree it _should_ work, but it doesn't in the various experiments I tried.

* using a list instead of a finset: this is easy to implement, but as you said is further from the informal statement and I don't see any advantage (but I am happy to change my mind).

Sorry, fin_cases works with the list (I am almost sure it didn't three hours ago... I don't know). So let's go with it.

May 28 '24 19:05 riccardobrasca

Maybe I should have put everything together in one big "suggestion" comment. It looks like it works after all changes are made (I had checked out your branch and changed the proof there, so the version I had was definitely working, but I may have made the odd copy-and-paste error when logging the suggestions). Sorry for the confusion!