Commit 2024-06-21 12:03 0be623ae

View on Github →

feat: Define the regulator of a number field (#12504) This PR defines the regulator of a number field K as the covolume of its unitLattice K. Basic results about the regulator are proved including the fact that it is equal to the absolute value of the matrix with entries mult w * Real.log w (fundSystem K i) where fundSystem K is the fundamental system of units and w runs through all the infinite places of K but one.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Ring/NegOnePow.lean

added theorem Int.abs_negOnePow

Modified Mathlib/GroupTheory/Perm/Sign.lean

added theorem Equiv.Perm.sign_abs

Modified Mathlib/NumberTheory/NumberField/Units/Basic.lean

Modified Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean

added theorem NumberField.Units.dirichletUnitTheorem.fundSystem_mk

deleted def NumberField.Units.dirichletUnitTheorem.logEmbedding

added def NumberField.Units.dirichletUnitTheorem.logEmbeddingEquiv

added theorem NumberField.Units.dirichletUnitTheorem.logEmbeddingEquiv_apply

added def NumberField.Units.dirichletUnitTheorem.logEmbeddingQuot

added theorem NumberField.Units.dirichletUnitTheorem.logEmbeddingQuot_apply

added theorem NumberField.Units.dirichletUnitTheorem.logEmbeddingQuot_injective

deleted def NumberField.Units.dirichletUnitTheorem.unitLatticeEquiv

added def NumberField.Units.logEmbedding

Created Mathlib/NumberTheory/NumberField/Units/Regulator.lean

added theorem NumberField.Units.abs_det_eq_abs_det

added def NumberField.Units.regulator

added theorem NumberField.Units.regulator_eq_det'

added theorem NumberField.Units.regulator_eq_det

added theorem NumberField.Units.regulator_ne_zero

added theorem NumberField.Units.regulator_pos