Commit 2026-01-19 09:42 519996e1

View on Github →

feat(NumberTheory/Height): heights of tuples and finsupps (#33893) This is the second PR on heights. We add the definition of the height of a tuple of field elements (and of finitely supported maps into the field) and prove some properties, for example the invariance under scaling by a nonzero field element.

Estimated changes

Modified Mathlib/NumberTheory/Height/Basic.lean

added def Finsupp.logHeight

added theorem Finsupp.logHeight_eq_log_mulHeight

added def Finsupp.mulHeight

added def Height.logHeight

added theorem Height.logHeight_eq_log_mulHeight

added theorem Height.logHeight_pow

added theorem Height.logHeight_smul_eq_logHeight

added theorem Height.logHeight₁_div_eq_logHeight

added theorem Height.logHeight₁_eq_logHeight

added theorem Height.logHeight₁_inv

added theorem Height.logHeight₁_pow

added theorem Height.logHeight₁_zpow

added theorem Height.mulHeight.ne_zero

added def Height.mulHeight

added theorem Height.mulHeight_comp_equiv

added theorem Height.mulHeight_eq

added theorem Height.mulHeight_one

added theorem Height.mulHeight_pos

added theorem Height.mulHeight_pow

added theorem Height.mulHeight_smul_eq_mulHeight

added theorem Height.mulHeight_swap

added theorem Height.mulHeight_zero

added theorem Height.mulHeight₁_div_eq_mulHeight

added theorem Height.mulHeight₁_eq_mulHeight

added theorem Height.mulHeight₁_inv

added theorem Height.mulHeight₁_pow

added theorem Height.mulHeight₁_zpow

added theorem Height.one_le_mulHeight

added theorem Height.zero_le_logHeight

Modified Mathlib/NumberTheory/Height/Instances.lean

added theorem NumberField.mulHeight_eq