Theorems · Theorem · number theory

NumberField.Units.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)),
  NumberField.Units.regulator K =
    |(Matrix.of fun i w =>
          ↑(↑w).mult *
            Real.log (↑w ((algebraMap (NumberField.RingOfIntegers K) K) ↑(NumberField.Units.fundSystem K (e i))))).det|

For any infinite place w', the regulator is equal to the absolute value of the determinant of the matrix with entries (mult w * log w (fundSystem K i))_i for 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