Kummer's Criterion and Regular Primes in Lean

7. Cyclotomic units and the plus class number🔗

This chapter records the cyclotomic-unit part of the proof. The purpose is to connect Bernoulli non-divisibility with the plus class number. Throughout this chapter p is an odd prime, K is a field isomorphic to \mathbb{Q}(\zeta_p), and K^+ = \mathbb{Q}(\zeta_p)^+ is its maximal real subfield. The group of real units is E^+ := (\mathcal{O}_{K^+})^\times. Thus E^+ is the full unit group of the maximal real subfield.

  1. 7.1. Real cyclotomic units
  2. 7.2. The cyclotomic-unit subgroups
  3. 7.3. Exact p-saturation
  4. 7.4. From saturation to index non-divisibility
  5. 7.5. The Kummer logarithm determinant
  6. 7.6. Bernoulli non-divisibility and the plus index
  7. 7.7. The needed Sinnott index formula