Commit 2023-11-04 10:04 3fdde997

feat: explicit volume computations in NumberTheory.NumberField.CanonicalEmbedding (#6886) We compute the values of the volumes used in CanonicalEmbedding. In particular, we prove that

volume (fundamentalDomain (latticeBasis K)) =
       (2 : ℝ≥0∞)⁻¹ ^ (NrComplexPlaces K) * NNReal.sqrt ‖discr K‖₊

This will be useful later on to prove Hermite and Hermite-Minkowski theorems.