Theorems · Theorem · number theory

NumberField.Units.finrank_mul_regOfFamily_eq_det

∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  (u : Fin (NumberField.Units.rank K) → (NumberField.RingOfIntegers K)ˣ) (w' : NumberField.InfinitePlace K)
  (e : { w // w ≠ w' } ≃ Fin (NumberField.Units.rank K)),
  ↑(Module.finrank ℚ K) * NumberField.Units.regOfFamily u =
    |(Matrix.of fun i w =>
          if h : i = w' then ↑w.mult
          else ↑w.mult * Real.log (w ((algebraMap (NumberField.RingOfIntegers K) K) ↑(u (e ⟨i, h⟩))))).det|

The degree of K times the regulator of the family u is equal to the absolute value of the determinant of the matrix whose columns are (mult w * log w (fundSystem K i))_i, w and the column (mult w)_w.

Defined in

Mathlib.NumberTheory.NumberField.Units.Regulator

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldNumberField