Kummer's lemma for regular primes

This file proves the unit form of Kummer's lemma for regular primes.

theorem exists_pow_eq_of_zeta_sub_one_pow_dvd_sub_one {K : Type} {p : ℕ} [hpri : Fact (Nat.Prime p)] [Field K] [NumberField K] (hp : p ≠ 2) [Fintype (ClassGroup (NumberField.RingOfIntegers K))] (hreg : p.Coprime (Fintype.card (ClassGroup (NumberField.RingOfIntegers K)))) {ζ : K} (hζ : IsPrimitiveRoot ζ p) {u : (NumberField.RingOfIntegers K)ˣ} (hcong : (hζ.toInteger - 1) ^ p ∣ ↑u - 1) : ∃ (v : K), v ^ p = (algebraMap (NumberField.RingOfIntegers K) K) ↑u

theorem eq_pow_prime_of_unit_of_congruent {K : Type} {p : ℕ} [hpri : Fact (Nat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) [Fintype (ClassGroup (NumberField.RingOfIntegers K))] (hreg : p.Coprime (Fintype.card (ClassGroup (NumberField.RingOfIntegers K)))) (u : (NumberField.RingOfIntegers K)ˣ) (hcong : ∃ (n : ℤ), ↑p ∣ ↑u - ↑n) : ∃ (v : (NumberField.RingOfIntegers K)ˣ), u = v ^ p

A regular prime criterion: if a unit of the cyclotomic field is congruent to an integer modulo p, then it is a p-th power.