Theorems · Theorem · number theory

NumberField.Units.abs_det_eq_abs_det

∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  (u : Fin (NumberField.Units.rank K) → (NumberField.RingOfIntegers K)ˣ) {w₁ w₂ : NumberField.InfinitePlace K}
  (e₁ : { w // w ≠ w₁ } ≃ Fin (NumberField.Units.rank K)) (e₂ : { w // w ≠ w₂ } ≃ Fin (NumberField.Units.rank K)),
  |(Matrix.of fun i w => ↑(↑w).mult * Real.log (↑w ((algebraMap (NumberField.RingOfIntegers K) K) ↑(u (e₁ i))))).det| =
    |(Matrix.of fun i w => ↑(↑w).mult * Real.log (↑w ((algebraMap (NumberField.RingOfIntegers K) K) ↑(u (e₂ i))))).det|

Let u : Fin (rank K) → (𝓞 K)ˣ be a family of units and let w₁ and w₂ be two infinite places. Then, the two square matrices with entries (mult w * log w (u i))_i where w ≠ w_j for j = 1, 2 have the same determinant in absolute value.

Defined in

Mathlib.NumberTheory.NumberField.Units.Regulator

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldNumberField