English
Dirichlet’s Unit Theorem asserts that every unit x ∈ (𝓞 K)× can be written uniquely as a product of a torsion element and integer powers of the fundamental system, i.e., x = ζe · ∏i (fundSystem K i)^{ζe.2 i} with ζe ∈ torsion K × (Fin(rank K) → ℤ).
Русский
Теорема Дирихле о единицах утверждает, что любая единица x ∈ (𝓞 K)× распадается единственным образом как произведение torsion-элемента и целочисленных степеней фундаментальной системы: x = ζe · ∏i (fundSystem K i)^{ζe.2 i}, где ζe ∈ torsion K × (Fin(rank K) → ℤ).
LaTeX
$$$\\forall K [Field K] [NumberField K], \\forall x \\in (\\mathcal{O}_K)^{\\times}, \\exists! \\zeta_e \\in \\mathrm{torsion}(K) \\times (\\mathrm{Fin}(\\mathrm{rank}\\,K) \\to \\mathbb{Z}), x = \\zeta_e.1 \\cdot \\prod_i (\\mathrm{fundSystem}~K~i)^{\\zeta_e.2(i)}.$$$
Lean4
/-- **Dirichlet Unit Theorem**. Any unit `x` of `𝓞 K` can be written uniquely as the product of
a root of unity and powers of the units of the fundamental system `fundSystem`. -/
theorem exist_unique_eq_mul_prod (x : (𝓞 K)ˣ) :
∃! ζe : torsion K × (Fin (rank K) → ℤ), x = ζe.1 * ∏ i, (fundSystem K i) ^ (ζe.2 i) :=
by
let ζ := x * (∏ i, (fundSystem K i) ^ ((basisModTorsion K).repr (Additive.ofMul ↑x) i))⁻¹
have h_tors : ζ ∈ torsion K :=
by
rw [← QuotientGroup.eq_one_iff, QuotientGroup.mk_mul, QuotientGroup.mk_inv, ← ofMul_eq_zero, ofMul_mul, ofMul_inv,
QuotientGroup.mk_prod, ofMul_prod]
simp_rw [QuotientGroup.mk_zpow, ofMul_zpow, fundSystem, QuotientGroup.out_eq']
rw [add_eq_zero_iff_eq_neg, neg_neg]
exact ((basisModTorsion K).sum_repr (Additive.ofMul ↑x)).symm
refine ⟨⟨⟨ζ, h_tors⟩, ((basisModTorsion K).repr (Additive.ofMul ↑x) : Fin (rank K) → ℤ)⟩, ?_, ?_⟩
· simp only [ζ, _root_.inv_mul_cancel_right]
· rintro ⟨⟨ζ', h_tors'⟩, η⟩ hf
simp only [ζ, ← fun_eq_repr K h_tors' hf, Prod.mk.injEq, Subtype.mk.injEq, and_true]
nth_rewrite 1 [hf]
rw [_root_.mul_inv_cancel_right]
