Theorems · Theorem · number theory

NumberField.det_basisOfFractionalIdeal_eq_absNorm

∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ)
  (e : Module.Free.ChooseBasisIndex ℤ (NumberField.RingOfIntegers K) ≃ Module.Free.ChooseBasisIndex ℤ ↥↑↑I),
  |(NumberField.integralBasis K).det ⇑((NumberField.basisOfFractionalIdeal K I).reindex e.symm)| =
    FractionalIdeal.absNorm ↑I

The absolute value of the determinant of the base change from integralBasis to basisOfFractionalIdeal I is equal to the norm of I.

Defined in

Mathlib.NumberTheory.NumberField.FractionalIdeal

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldNumberField