Commit 2026-03-04 14:59 c3264983

View on Github →

feat(NumberTheory/Height/Basic): add {mul|log}Height_comp_le, {mul|log}Height_fun_mul_eq (#35408) This adds

  • two missing logHeight lemmas (their mulHeight versions are already there)
  • {mul|log}Height_comp_le: the height of x ∘ f is bounded by the height of x
  • {mul|log}Height_fun_mul_eq: the height of the "multiplication table" fun (i, j) ↦ x i * y j is the {product|sum} of the heights of x and of y
  • {mul|log}Height_fun_prod_eq: the analogous result for products with arbitrarily many factors
  • plus some API lemmas needed for these.

Estimated changes

added theorem Finite.ciInf_prod
added theorem Finite.ciSup_prod
modified theorem Height.logHeight_one
added theorem Height.logHeight_swap
modified theorem Height.logHeight_zero
modified theorem Height.mulHeight_comp_equiv
added theorem ciInf_prod
added theorem ciSup_prod