NumberField.det_basisOfFractionalIdeal_eq_absNorm

theorem 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 theorem `NumberField.det_basisOfFractionalIdeal_eq_absNorm` states that for any number field `K`, and any invertible fractional ideal `I` of `K` (over the non-zero divisors of the ring of integers of `K`), for any equivalence `e` between the index set of the integral basis of `K` over the integers and the index set of the `ℚ`-basis of `K` that spans `I` over the integers, the absolute value of the determinant of the base change from the integral basis to the `ℚ`-basis that spans `I` is equal to the norm of `I`. In other words, the determinant of the transformation between these bases, in absolute value, exactly measures the norm of the fractional ideal `I`.

More concisely: For any number field K and invertible fractional ideal I, the absolute value of the determinant of the base change matrix from the integral basis to the basis of I over the integers equals the norm of I.