Theorems · Theorem · number theory

NumberField.Units.finrank_mul_regulator_eq_det

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

The degree of K times the regulator of K 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

0 results in Mathlib

Foundations

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

Assumes

FieldNumberField