Commit 2026-02-16 07:36 4c9ff108

View on Github →

feat(NumberTheory/Height/Basic): add bounds for sums (#34330) The main purpose of this PR (no. 3 in the series on heights) is to state and prove bounds for the height of x + y and for the height of a finite sum of field elements.

Estimated changes

Modified Mathlib/Algebra/Order/BigOperators/GroupWithZero/Multiset.lean

added theorem Multiset.one_le_prod_map

added theorem Multiset.prod_map_nonneg

Modified Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean

added theorem Finset.le_prod_max_one

Modified Mathlib/NumberTheory/Height/Basic.lean

added theorem Finset.max_abv_sum_one_le

added theorem Finset.max_abv_sum_one_le_of_isNonarchimedean

added theorem Height.logHeight₁_add_le

added theorem Height.logHeight₁_neg

added theorem Height.logHeight₁_sub_le

added theorem Height.logHeight₁_sum_le

added theorem Height.mulHeight₁_add_le

added theorem Height.mulHeight₁_neg

added theorem Height.mulHeight₁_sub_le

added theorem Height.mulHeight₁_sum_le

modified theorem Height.one_le_mulHeight₁