Commit 2024-06-05 05:11 cdedc9bb

feat (Mathlib.NumberTheory.Cyclotomic.Three): new file (#12765) 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.