Commit 2023-09-27 14:09 2b8f139e
View on Github →feat(NumberTheory.NumberField.Units): proof of Dirichlet's unit theorem (#5960) We prove Dirichlet's unit theorem. More precisely, the main results are:
def basisModTorsion : Basis (Fin (Units.rank K)) ℤ (Additive ((𝓞 K)ˣ ⧸ (torsion K)))
where Units.rank := Fintype.card (InfinitePlace K) - 1
and
theorem exist_unique_eq_mul_prod (x : (𝓞 K)ˣ) : ∃! (ζ : torsion K) (e : Fin (Units.rank K) → ℤ),
x = ζ * ∏ i, (fundSystem K i) ^ (e i)
where fundSystem : Fin (rank K) → (𝓞 K)ˣ
is a fundamental system of units.
The exponents in exist_unique_eq_mul_prod
can be computed via the following result:
theorem fun_eq_repr {x ζ : (𝓞 K)ˣ} {f : Fin (rank K) → ℤ} (hζ : ζ ∈ torsion K)
(h : x = ζ * ∏ i, (fundSystem K i) ^ (f i)) : f = (basisModTorsion K).repr (Additive.ofMul ↑x)