Commit 2026-03-02 16:30 04cca157

View on Github →

feat(NumberTheory/Height): formula for logHeight₁ (#35919) This adds the formula for the logarithmic height of a field element as the sum of the positive parts of the logaithms of its various absolute values, plus a version specific for number fields. We also add an API lemma Real.log_finprod that is needed for this.

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/Log/Basic.lean

added theorem Real.log_finprod

Modified Mathlib/NumberTheory/Height/Basic.lean

added theorem Height.logHeight₁_eq

Modified Mathlib/NumberTheory/Height/NumberField.lean

added theorem NumberField.logHeight₁_eq

added theorem NumberField.sum_archAbsVal_eq

added theorem NumberField.sum_nonarchAbsVal_eq