Documentation

FLT3.Mathlib.NumberTheory.NumberField.Units

Units of a number field #

We prove results about the group (π“ž K)Λ£ of units of the ring of integers π“ž K of a number field K.

Main definitions #

Main results #

Tags #

number field, units

source
theorem Rat.RingOfIntegers.isUnit_iff {x : β†₯(NumberField.ringOfIntegers β„š)} :
IsUnit x ↔ ↑x = 1 ∨ ↑x = -1
source
theorem NumberField.isUnit_iff_norm {K : Type u_1} [Field K] [NumberField K] {x : β†₯(NumberField.ringOfIntegers K)} :
IsUnit x ↔ |↑((RingOfIntegers.norm β„š) x)| = 1
source
theorem NumberField.Units.coe_injective (K : Type u_1) [Field K] :
Function.Injective fun (x : (β†₯(NumberField.ringOfIntegers K))Λ£) => ↑↑x
source
theorem NumberField.Units.coe_mul {K : Type u_1} [Field K] (x : (β†₯(NumberField.ringOfIntegers K))Λ£) (y : (β†₯(NumberField.ringOfIntegers K))Λ£) :
↑↑(x * y) = ↑↑x * ↑↑y
source
theorem NumberField.Units.coe_pow {K : Type u_1} [Field K] (x : (β†₯(NumberField.ringOfIntegers K))Λ£) (n : β„•) :
↑↑(x ^ n) = ↑↑x ^ n
source
theorem NumberField.Units.coe_zpow {K : Type u_1} [Field K] (x : (β†₯(NumberField.ringOfIntegers K))Λ£) (n : β„€) :
↑↑(x ^ n) = ↑↑x ^ n
source
theorem NumberField.Units.coe_one {K : Type u_1} [Field K] :
↑↑1 = 1
source
theorem NumberField.Units.coe_neg_one {K : Type u_1} [Field K] :
↑↑(-1) = -1
source
theorem NumberField.Units.coe_ne_zero {K : Type u_1} [Field K] (x : (β†₯(NumberField.ringOfIntegers K))Λ£) :
↑↑x β‰  0
source
def NumberField.Units.torsion (K : Type u_1) [Field K] :
Subgroup (β†₯(NumberField.ringOfIntegers K))Λ£

The torsion subgroup of the group of units.

Equations
Instances For
    source
    theorem NumberField.Units.mem_torsion (K : Type u_1) [Field K] {x : (β†₯(NumberField.ringOfIntegers K))Λ£} [NumberField K] :
    x ∈ NumberField.Units.torsion K ↔ βˆ€ (w : NumberField.InfinitePlace K), w ↑↑x = 1
    source
    instance NumberField.Units.instNonemptySubtypeUnitsMemSubalgebraIntToCommSemiringInstCommRingIntToSemiringToCommSemiringToCommRingToEuclideanDomainAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersToMonoidToMonoidToMonoidWithZeroToSemiringToDivisionSemiringToSemifieldToSubmonoidToNonAssocSemiringToSubsemiringSubgroupInstGroupInstSetLikeSubgroupTorsion (K : Type u_1) [Field K] :
    Nonempty β†₯(NumberField.Units.torsion K)

    Shortcut instance because Lean tends to time out before finding the general instance.

    Equations
    • β‹― = β‹―
    source
    instance NumberField.Units.instFintypeSubtypeUnitsMemSubalgebraIntToCommSemiringInstCommRingIntToSemiringToCommSemiringToCommRingToEuclideanDomainAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersToMonoidToMonoidToMonoidWithZeroToSemiringToDivisionSemiringToSemifieldToSubmonoidToNonAssocSemiringToSubsemiringSubgroupInstGroupInstSetLikeSubgroupTorsion (K : Type u_1) [Field K] [NumberField K] :
    Fintype β†₯(NumberField.Units.torsion K)

    The torsion subgroup is finite.

    Equations
    • One or more equations did not get rendered due to their size.
    source
    instance NumberField.Units.instFiniteSubtypeUnitsMemSubalgebraIntToCommSemiringInstCommRingIntToSemiringToCommSemiringToCommRingToEuclideanDomainAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersToMonoidToMonoidToMonoidWithZeroToSemiringToDivisionSemiringToSemifieldToSubmonoidToNonAssocSemiringToSubsemiringSubgroupInstGroupInstSetLikeSubgroupTorsion (K : Type u_1) [Field K] [NumberField K] :
    Finite β†₯(NumberField.Units.torsion K)
    Equations
    • β‹― = β‹―
    source
    instance NumberField.Units.instIsCyclicSubtypeUnitsMemSubalgebraIntToCommSemiringInstCommRingIntToSemiringToCommSemiringToCommRingToEuclideanDomainAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersToMonoidToMonoidToMonoidWithZeroToSemiringToDivisionSemiringToSemifieldToSubmonoidToNonAssocSemiringToSubsemiringSubgroupInstGroupInstSetLikeSubgroupTorsionToGroup (K : Type u_1) [Field K] [NumberField K] :
    IsCyclic β†₯(NumberField.Units.torsion K)

    The torsion subgroup is cylic.

    Equations
    • β‹― = β‹―
    source
    def NumberField.Units.torsionOrder (K : Type u_1) [Field K] [NumberField K] :
    β„•+

    The order of the torsion subgroup as a positive integer.

    Equations
    Instances For
      source
      theorem NumberField.Units.rootsOfUnity_eq_one (K : Type u_1) [Field K] [NumberField K] {k : β„•+} (hc : Nat.Coprime ↑k ↑(NumberField.Units.torsionOrder K)) {ΞΆ : (β†₯(NumberField.ringOfIntegers K))Λ£} :
      ΞΆ ∈ rootsOfUnity k β†₯(NumberField.ringOfIntegers K) ↔ ΞΆ = 1

      If k does not divide torsionOrder then there are no nontrivial roots of unity of order dividing k.

      source
      theorem NumberField.Units.rootsOfUnity_eq_torsion (K : Type u_1) [Field K] [NumberField K] :
      rootsOfUnity (NumberField.Units.torsionOrder K) β†₯(NumberField.ringOfIntegers K) = NumberField.Units.torsion K

      The group of roots of unity of order dividing torsionOrder is equal to the torsion group.

      Dirichlet Unit Theorem #

      This section is devoted to the proof of Dirichlet's unit theorem.

      We define a group morphism from (π“ž K)Λ£ to {w : InfinitePlace K // w β‰  wβ‚€} β†’ ℝ where wβ‚€ is a distinguished (arbitrary) infinite place, prove that its kernel is the torsion subgroup (see logEmbedding_eq_zero_iff) and that its image, called unitLattice, is a full β„€-lattice. It follows that unitLattice is a free β„€-module (see instModuleFree_unitLattice) of rank card (InfinitePlaces K) - 1 (see unitLattice_rank). To prove that the unitLattice is a full β„€-lattice, we need to prove that it is discrete (see unitLattice_inter_ball_finite) and that it spans the full space over ℝ (see unitLattice_span_eq_top); this is the main part of the proof, see the section span_top below for more details.

      source
      def NumberField.Units.dirichletUnitTheorem.wβ‚€ {K : Type u_1} [Field K] [NumberField K] :
      NumberField.InfinitePlace K

      The distinguished infinite place.

      Equations
      • NumberField.Units.dirichletUnitTheorem.wβ‚€ = Nonempty.some β‹―
      Instances For
        source
        def NumberField.Units.dirichletUnitTheorem.logEmbedding (K : Type u_1) [Field K] [NumberField K] :
        Additive (β†₯(NumberField.ringOfIntegers K))Λ£ β†’+ { w : NumberField.InfinitePlace K // w β‰  NumberField.Units.dirichletUnitTheorem.wβ‚€ } β†’ ℝ

        The logarithmic embedding of the units (seen as an Additive group).

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem NumberField.Units.dirichletUnitTheorem.logEmbedding_component {K : Type u_1} [Field K] [NumberField K] (x : (β†₯(NumberField.ringOfIntegers K))Λ£) (w : { w : NumberField.InfinitePlace K // w β‰  NumberField.Units.dirichletUnitTheorem.wβ‚€ }) :
          (NumberField.Units.dirichletUnitTheorem.logEmbedding K) x w = ↑(NumberField.InfinitePlace.mult ↑w) * Real.log (↑w ↑↑x)
          source
          theorem NumberField.Units.dirichletUnitTheorem.sum_logEmbedding_component {K : Type u_1} [Field K] [NumberField K] (x : (β†₯(NumberField.ringOfIntegers K))Λ£) :
          (Finset.sum Finset.univ fun (w : { w : NumberField.InfinitePlace K // w β‰  NumberField.Units.dirichletUnitTheorem.wβ‚€ }) => (NumberField.Units.dirichletUnitTheorem.logEmbedding K) x w) = -↑(NumberField.InfinitePlace.mult NumberField.Units.dirichletUnitTheorem.wβ‚€) * Real.log (NumberField.Units.dirichletUnitTheorem.wβ‚€ ↑↑x)
          source
          theorem NumberField.Units.dirichletUnitTheorem.mult_log_place_eq_zero {K : Type u_1} [Field K] {x : (β†₯(NumberField.ringOfIntegers K))Λ£} {w : NumberField.InfinitePlace K} :
          ↑(NumberField.InfinitePlace.mult w) * Real.log (w ↑↑x) = 0 ↔ w ↑↑x = 1
          source
          theorem NumberField.Units.dirichletUnitTheorem.logEmbedding_eq_zero_iff {K : Type u_1} [Field K] [NumberField K] {x : (β†₯(NumberField.ringOfIntegers K))Λ£} :
          (NumberField.Units.dirichletUnitTheorem.logEmbedding K) x = 0 ↔ x ∈ NumberField.Units.torsion K
          source
          theorem NumberField.Units.dirichletUnitTheorem.logEmbedding_component_le {K : Type u_1} [Field K] [NumberField K] {r : ℝ} {x : (β†₯(NumberField.ringOfIntegers K))Λ£} (hr : 0 ≀ r) (h : β€–(NumberField.Units.dirichletUnitTheorem.logEmbedding K) xβ€– ≀ r) (w : { w : NumberField.InfinitePlace K // w β‰  NumberField.Units.dirichletUnitTheorem.wβ‚€ }) :
          |(NumberField.Units.dirichletUnitTheorem.logEmbedding K) x w| ≀ r
          source
          theorem NumberField.Units.dirichletUnitTheorem.log_le_of_logEmbedding_le {K : Type u_1} [Field K] [NumberField K] {r : ℝ} {x : (β†₯(NumberField.ringOfIntegers K))Λ£} (hr : 0 ≀ r) (h : β€–(NumberField.Units.dirichletUnitTheorem.logEmbedding K) xβ€– ≀ r) (w : NumberField.InfinitePlace K) :
          |Real.log (w ↑↑x)| ≀ ↑(Fintype.card (NumberField.InfinitePlace K)) * r
          source
          noncomputable def NumberField.Units.unitLattice (K : Type u_1) [Field K] [NumberField K] :
          AddSubgroup ({ w : NumberField.InfinitePlace K // w β‰  NumberField.Units.dirichletUnitTheorem.wβ‚€ } β†’ ℝ)

          The lattice formed by the image of the logarithmic embedding.

          Equations
          Instances For
            source
            theorem NumberField.Units.dirichletUnitTheorem.unitLattice_inter_ball_finite (K : Type u_1) [Field K] [NumberField K] (r : ℝ) :
            Set.Finite (↑(NumberField.Units.unitLattice K) ∩ Metric.closedBall 0 r)

            Section span_top #

            In this section, we prove that the span over ℝ of the unitLattice is equal to the full space. For this, we construct for each infinite place w₁ β‰  wβ‚€ a unit u_w₁ of K such that, for all infinite places w such that w β‰  w₁, we have Real.log w (u_w₁) < 0 (and thus Real.log w₁ (u_w₁) > 0). It follows then from a determinant computation (using Matrix.det_ne_zero_of_sum_col_lt_diag) that the image by logEmbedding of these units is a ℝ-linearly independent family. The unit u_w₁ is obtained by constructing a sequence seq n of nonzero algebraic integers that is strictly decreasing at infinite places distinct from w₁ and of norm ≀ B. Since there are finitely many ideals of norm ≀ B, there exists two term in the sequence defining the same ideal and their quotient is the desired unit u_w₁ (see exists_unit).

            source
            theorem NumberField.Units.dirichletUnitTheorem.seq_next (K : Type u_1) [Field K] [NumberField K] (w₁ : NumberField.InfinitePlace K) {B : β„•} (hB : NumberField.mixedEmbedding.minkowskiBound K 1 < ↑(NumberField.mixedEmbedding.convexBodyLTFactor K) * ↑B) {x : β†₯(NumberField.ringOfIntegers K)} (hx : x β‰  0) :
            βˆƒ (y : β†₯(NumberField.ringOfIntegers K)), y β‰  0 ∧ (βˆ€ (w : NumberField.InfinitePlace K), w β‰  w₁ β†’ w ↑y < w ↑x) ∧ |(Algebra.norm β„š) ↑y| ≀ ↑B

            This result shows that there always exists a next term in the sequence.

            source
            def NumberField.Units.dirichletUnitTheorem.seq (K : Type u_1) [Field K] [NumberField K] (w₁ : NumberField.InfinitePlace K) {B : β„•} (hB : NumberField.mixedEmbedding.minkowskiBound K 1 < ↑(NumberField.mixedEmbedding.convexBodyLTFactor K) * ↑B) :
            β„• β†’ { x : β†₯(NumberField.ringOfIntegers K) // x β‰  0 }

            An infinite sequence of nonzero algebraic integers of K satisfying the following properties: β€’ seq n is nonzero; β€’ for w : InfinitePlace K, w β‰  w₁ β†’ w (seq n+1) < w (seq n); β€’ ∣norm (seq n)∣ ≀ B.

            Equations
            Instances For
              source
              theorem NumberField.Units.dirichletUnitTheorem.seq_ne_zero (K : Type u_1) [Field K] [NumberField K] (w₁ : NumberField.InfinitePlace K) {B : β„•} (hB : NumberField.mixedEmbedding.minkowskiBound K 1 < ↑(NumberField.mixedEmbedding.convexBodyLTFactor K) * ↑B) (n : β„•) :
              ↑↑(NumberField.Units.dirichletUnitTheorem.seq K w₁ hB n) β‰  0

              The terms of the sequence are nonzero.

              source
              theorem NumberField.Units.dirichletUnitTheorem.seq_norm_ne_zero (K : Type u_1) [Field K] [NumberField K] (w₁ : NumberField.InfinitePlace K) {B : β„•} (hB : NumberField.mixedEmbedding.minkowskiBound K 1 < ↑(NumberField.mixedEmbedding.convexBodyLTFactor K) * ↑B) (n : β„•) :
              (Algebra.norm β„€) ↑(NumberField.Units.dirichletUnitTheorem.seq K w₁ hB n) β‰  0

              The terms of the sequence have nonzero norm.

              source
              theorem NumberField.Units.dirichletUnitTheorem.seq_decreasing (K : Type u_1) [Field K] [NumberField K] (w₁ : NumberField.InfinitePlace K) {B : β„•} (hB : NumberField.mixedEmbedding.minkowskiBound K 1 < ↑(NumberField.mixedEmbedding.convexBodyLTFactor K) * ↑B) {n : β„•} {m : β„•} (h : n < m) (w : NumberField.InfinitePlace K) (hw : w β‰  w₁) :
              w ↑↑(NumberField.Units.dirichletUnitTheorem.seq K w₁ hB m) < w ↑↑(NumberField.Units.dirichletUnitTheorem.seq K w₁ hB n)

              The sequence is strictly decreasing at infinite places distinct from w₁.

              source
              theorem NumberField.Units.dirichletUnitTheorem.seq_norm_le (K : Type u_1) [Field K] [NumberField K] (w₁ : NumberField.InfinitePlace K) {B : β„•} (hB : NumberField.mixedEmbedding.minkowskiBound K 1 < ↑(NumberField.mixedEmbedding.convexBodyLTFactor K) * ↑B) (n : β„•) :
              Int.natAbs ((Algebra.norm β„€) ↑(NumberField.Units.dirichletUnitTheorem.seq K w₁ hB n)) ≀ B

              The terms of the sequence have norm bounded by B.

              source
              theorem NumberField.Units.dirichletUnitTheorem.exists_unit (K : Type u_1) [Field K] [NumberField K] (w₁ : NumberField.InfinitePlace K) :
              βˆƒ (u : (β†₯(NumberField.ringOfIntegers K))Λ£), βˆ€ (w : NumberField.InfinitePlace K), w β‰  w₁ β†’ Real.log (w ↑↑u) < 0

              Construct a unit associated to the place w₁. The family, for w₁ β‰  wβ‚€, formed by the image by the logEmbedding of these units is ℝ-linearly independent, see unitLattice_span_eq_top.

              source
              theorem NumberField.Units.dirichletUnitTheorem.unitLattice_span_eq_top (K : Type u_1) [Field K] [NumberField K] :
              Submodule.span ℝ ↑(NumberField.Units.unitLattice K) = ⊀
              source
              def NumberField.Units.rank (K : Type u_1) [Field K] [NumberField K] :
              β„•

              The unit rank of the number field K, it is equal to card (InfinitePlace K) - 1.

              Equations
              Instances For
                source
                instance NumberField.Units.instDiscrete_unitLattice (K : Type u_1) [Field K] [NumberField K] :
                DiscreteTopology β†₯(NumberField.Units.unitLattice K)
                Equations
                • β‹― = β‹―
                source
                instance NumberField.Units.instZlattice_unitLattice (K : Type u_1) [Field K] [NumberField K] :
                IsZlattice ℝ (NumberField.Units.unitLattice K)
                Equations
                • β‹― = β‹―
                source
                theorem NumberField.Units.finrank_eq_rank (K : Type u_1) [Field K] [NumberField K] :
                FiniteDimensional.finrank ℝ ({ w : NumberField.InfinitePlace K // w β‰  NumberField.Units.dirichletUnitTheorem.wβ‚€ } β†’ ℝ) = NumberField.Units.rank K
                source
                @[simp]
                theorem NumberField.Units.unitLattice_rank (K : Type u_1) [Field K] [NumberField K] :
                FiniteDimensional.finrank β„€ β†₯(NumberField.Units.unitLattice K) = NumberField.Units.rank K
                source
                def NumberField.Units.unitLatticeEquiv (K : Type u_1) [Field K] [NumberField K] :
                β†₯(NumberField.Units.unitLattice K) ≃ₗ[β„€] Additive ((β†₯(NumberField.ringOfIntegers K))Λ£ β§Έ NumberField.Units.torsion K)

                The linear equivalence between unitLattice and (π“ž K)Λ£ β§Έ (torsion K) as an additive β„€-module.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  instance NumberField.Units.instFreeIntAdditiveQuotientUnitsSubtypeMemSubalgebraToCommSemiringInstCommRingIntToSemiringToCommSemiringToCommRingToEuclideanDomainAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersToMonoidToMonoidToMonoidWithZeroToSemiringToDivisionSemiringToSemifieldToSubmonoidToNonAssocSemiringToSubsemiringSubgroupInstGroupInstHasQuotientSubgroupTorsionInstSemiringIntAddCommMonoidToCommMonoidCommGroupInstCommGroupUnitsToCommMonoidToCommRingToCommRingIntModuleAddCommGroup (K : Type u_1) [Field K] [NumberField K] :
                  Module.Free β„€ (Additive ((β†₯(NumberField.ringOfIntegers K))Λ£ β§Έ NumberField.Units.torsion K))
                  Equations
                  • β‹― = β‹―
                  source
                  instance NumberField.Units.instFiniteIntAdditiveQuotientUnitsSubtypeMemSubalgebraToCommSemiringInstCommRingIntToSemiringToCommSemiringToCommRingToEuclideanDomainAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersToMonoidToMonoidToMonoidWithZeroToSemiringToDivisionSemiringToSemifieldToSubmonoidToNonAssocSemiringToSubsemiringSubgroupInstGroupInstHasQuotientSubgroupTorsionInstSemiringIntAddCommMonoidToCommMonoidCommGroupInstCommGroupUnitsToCommMonoidToCommRingToCommRingIntModuleAddCommGroup (K : Type u_1) [Field K] [NumberField K] :
                  Module.Finite β„€ (Additive ((β†₯(NumberField.ringOfIntegers K))Λ£ β§Έ NumberField.Units.torsion K))
                  Equations
                  • β‹― = β‹―
                  source
                  instance NumberField.Units.instFiniteIntAdditiveUnitsSubtypeMemSubalgebraToCommSemiringInstCommRingIntToSemiringToCommSemiringToCommRingToEuclideanDomainAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersToMonoidToMonoidToMonoidWithZeroToSemiringToDivisionSemiringToSemifieldToSubmonoidToNonAssocSemiringToSubsemiringInstSemiringIntAddCommMonoidToCommMonoidInstCommGroupUnitsToCommMonoidToCommMonoidIntModuleAddCommGroup (K : Type u_1) [Field K] [NumberField K] :
                  Module.Finite β„€ (Additive (β†₯(NumberField.ringOfIntegers K))Λ£)
                  Equations
                  • β‹― = β‹―
                  source
                  instance NumberField.Units.instFGUnitsSubtypeMemSubalgebraIntToCommSemiringInstCommRingIntToSemiringToCommSemiringToCommRingToEuclideanDomainAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersToMonoidToMonoidToMonoidWithZeroToSemiringToDivisionSemiringToSemifieldToSubmonoidToNonAssocSemiringToSubsemiringInstMonoid (K : Type u_1) [Field K] [NumberField K] :
                  Monoid.FG (β†₯(NumberField.ringOfIntegers K))Λ£
                  Equations
                  • β‹― = β‹―
                  source
                  theorem NumberField.Units.rank_modTorsion (K : Type u_1) [Field K] [NumberField K] :
                  FiniteDimensional.finrank β„€ (Additive ((β†₯(NumberField.ringOfIntegers K))Λ£ β§Έ NumberField.Units.torsion K)) = NumberField.Units.rank K
                  source
                  def NumberField.Units.basisModTorsion (K : Type u_1) [Field K] [NumberField K] :
                  Basis (Fin (NumberField.Units.rank K)) β„€ (Additive ((β†₯(NumberField.ringOfIntegers K))Λ£ β§Έ NumberField.Units.torsion K))

                  A basis of the quotient (π“ž K)Λ£ β§Έ (torsion K) seen as an additive β„€-module.

                  Equations
                  Instances For
                    source
                    def NumberField.Units.fundSystem (K : Type u_1) [Field K] [NumberField K] :
                    Fin (NumberField.Units.rank K) β†’ (β†₯(NumberField.ringOfIntegers K))Λ£

                    A fundamental system of units of K. The units of fundSystem are arbitrary lifts of the units in basisModTorsion.

                    Equations
                    Instances For
                      source
                      theorem NumberField.Units.fun_eq_repr (K : Type u_1) [Field K] [NumberField K] {x : (β†₯(NumberField.ringOfIntegers K))Λ£} {ΞΆ : (β†₯(NumberField.ringOfIntegers K))Λ£} {f : Fin (NumberField.Units.rank K) β†’ β„€} (hΞΆ : ΞΆ ∈ NumberField.Units.torsion K) (h : x = ΞΆ * Finset.prod Finset.univ fun (i : Fin (NumberField.Units.rank K)) => NumberField.Units.fundSystem K i ^ f i) :
                      f = ⇑((NumberField.Units.basisModTorsion K).repr (Additive.ofMul ↑x))

                      The exponents that appear in the unique decomposition of a unit as the product of a root of unity and powers of the units of the fundamental system fundSystem (see exist_unique_eq_mul_prod) are given by the representation of the unit on basisModTorsion.

                      source
                      theorem NumberField.Units.exist_unique_eq_mul_prod (K : Type u_1) [Field K] [NumberField K] (x : (β†₯(NumberField.ringOfIntegers K))Λ£) :
                      βˆƒ! (ΞΆ : β†₯(NumberField.Units.torsion K)), βˆƒ! (e : Fin (NumberField.Units.rank K) β†’ β„€), x = ↑΢ * Finset.prod Finset.univ fun (i : Fin (NumberField.Units.rank K)) => NumberField.Units.fundSystem K i ^ e i

                      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.