Theorems · Theorem · number theory

NumberField.Units.fun_eq_repr

∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] {x ζ : (NumberField.RingOfIntegers K)ˣ}
  {f : Fin (NumberField.Units.rank K) → ℤ},
  ζ ∈ NumberField.Units.torsion K →
    x = ζ * ∏ i, 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.

Defined in

Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Cited by

1 results in Mathlib

Foundations

Depth 325 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldNumberField