PrimaryRootsDivisibility.lean

theorem exists_primitiveRoot_prime_pow_of_infinite_primary
    (p : ℕ) [Fact p.Prime] [Infinite (CommGroup.primaryComponent Kˣ p)] (n : ℕ) :
    ∃ ζ : Kˣ, IsPrimitiveRoot ζ (p ^ n)

theorem primaryComponent_prime_pow_surjective_of_infinite
    (p : ℕ) [Fact p.Prime] [Infinite (CommGroup.primaryComponent Kˣ p)]
    (q : ℕ) (hq : q.Prime) :
    Function.Surjective (fun z : CommGroup.primaryComponent Kˣ p => z ^ q) := by
  intro z
  have hp : p.Prime := Fact.out
  obtain ⟨m, hm⟩ := CommGroup.mem_primaryComponent_iff_orderOf.mp z.property
  by_cases hqp : q = p
  · subst q
    obtain ⟨η, hη⟩ := exists_primitiveRoot_prime_pow_of_infinite_primary (K := K) p (m + 1)
    have hηp : IsPrimitiveRoot (η ^ p) (p ^ m) :=
      hη.pow (pow_pos hp.pos (m + 1)) (by rw [pow_succ, mul_comm])
    have hzpow : (z : Kˣ) ^ (p ^ m) = 1 := by rw [← hm, pow_orderOf_eq_one]
    let : NeZero (p ^ m) := ⟨pow_ne_zero m hp.ne_zero⟩
    obtain ⟨i, _, hi⟩ := hηp.eq_pow_of_mem_rootsOfUnity
      ((mem_rootsOfUnity (p ^ m) (z : Kˣ)).mpr hzpow)
    have hηmem : η ∈ CommGroup.primaryComponent Kˣ p := ⟨m + 1, hη.pow_eq_one⟩
    refine ⟨⟨η ^ i, (CommGroup.primaryComponent Kˣ p).pow_mem hηmem i⟩, ?_⟩
    apply Subtype.ext
    change (η ^ i) ^ p = (z : Kˣ)
    rw [pow_right_comm]
    exact hi
  · have hcop : q.Coprime (orderOf z) := by
      have hm' : orderOf z = p ^ m := by simpa only [orderOf_submonoid] using hm
      rw [hm']
      exact ((hq.coprime_iff_not_dvd).mpr
        (fun h => hqp ((Nat.prime_dvd_prime_iff_eq hq hp).mp h))).pow_right m
    obtain ⟨i, hi⟩ := exists_pow_eq_self_of_coprime (x := z) hcop
    refine ⟨z ^ i, ?_⟩
    change (z ^ i) ^ q = z
    rw [pow_right_comm]
    exact hi

theorem primaryComponent_pow_surjective_of_infinite
    (p : ℕ) [Fact p.Prime] [Infinite (CommGroup.primaryComponent Kˣ p)]
    (n : ℕ) (hn : 0 < n) :
    Function.Surjective (fun z : CommGroup.primaryComponent Kˣ p => z ^ n) := by
  induction n using Nat.strong_induction_on with
  | h n ih =>
    by_cases hn1 : n = 1
    · subst n
      intro z
      exact ⟨z, pow_one z⟩
    obtain ⟨q, hq, hqn⟩ := Nat.exists_prime_and_dvd (by omega : n ≠ 1)
    have hdivpos : 0 < n / q := Nat.div_pos (Nat.le_of_dvd hn hqn) hq.pos
    have hdivlt : n / q < n := Nat.div_lt_self hn hq.one_lt
    intro z
    obtain ⟨y, hy⟩ := ih (n / q) hdivlt hdivpos z
    obtain ⟨x, hx⟩ := primaryComponent_prime_pow_surjective_of_infinite p q hq y
    refine ⟨x, ?_⟩
    change x ^ n = z
    rw [← Nat.mul_div_cancel' hqn, pow_mul]
    exact (congrArg (fun a => a ^ (n / q)) hx).trans hy

theorem finite_primaryComponent_of_no_infinitely_divisible_units
    (hK : ∀ z : Kˣ, (∀ n : ℕ, 0 < n → ∃ y : Kˣ, y ^ n = z) → z = 1)
    (p : ℕ) [Fact p.Prime] :
    Finite (CommGroup.primaryComponent Kˣ p)