feat(NumberTheory.NumberField.Units): proof of Dirichlet's unit theorem (#5960)

We prove Dirichlet's unit theorem. More precisely, the main results are:
```lean
def basisModTorsion : Basis (Fin (Units.rank K)) ℤ (Additive ((𝓞 K)ˣ ⧸ (torsion K)))
```
where `Units.rank := Fintype.card (InfinitePlace K) - 1` and 
```lean 
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:
```lean
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)
```

Author: xroblot

Mathlib/GroupTheory/QuotientGroup.lean

@@ -191,6 +191,11 @@ theorem mk_zpow (a : G) (n : ℤ) : ((a ^ n : G) : Q ) = (a : Q) ^ n :=
 #align quotient_group.coe_zpow QuotientGroup.mk_zpow
 #align quotient_add_group.coe_zsmul QuotientAddGroup.mk_zsmul
 
+ @[to_additive (attr := simp)]
+ theorem mk_prod {G ι : Type _} [CommGroup G] (N : Subgroup G) (s : Finset ι) {f : ι → G} :
+     ((Finset.prod s f : G) : G ⧸ N) = Finset.prod s (fun i => (f i : G ⧸ N)) :=
+   map_prod (QuotientGroup.mk' N) _ _
+
 /-- A group homomorphism `φ : G →* M` with `N ⊆ ker(φ)` descends (i.e. `lift`s) to a
 group homomorphism `G/N →* M`. -/
 @[to_additive "An `AddGroup` homomorphism `φ : G →+ M` with `N ⊆ ker(φ)` descends (i.e. `lift`s)

Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean

@@ -329,7 +329,7 @@ noncomputable abbrev convexBodyLtFactor : ℝ≥0∞ :=
   (2 : ℝ≥0∞) ^ card {w : InfinitePlace K // IsReal w} *
     volume (ball (0 : ℂ) 1) ^ card {w : InfinitePlace K // IsComplex w}
 
-theorem convexBodyLtFactor_lt_pos : 0 < (convexBodyLtFactor K) := by
+theorem convexBodyLtFactor_pos : 0 < (convexBodyLtFactor K) := by
   refine mul_pos (NeZero.ne _) ?_
   exact ENNReal.pow_ne_zero (ne_of_gt (measure_ball_pos _ _ (by norm_num))) _