Commit 2026-01-05 16:12 477c7fe3

feat(NumberTheory/Height/Basic): first installment of heights (#33054) This is the first PR in a series that aims at providing heights (in the sense of arithmetic geometry). Here we define a class Height.AdmissibleAbsValues that captures a family of "admissible" absolute values (finitely many archimedean ones, an arbitrary family of nonarchimedean ones, satisfying a finiteness condition and a product formula) and define the multiplicative and the logarithmic height of an element of a field K endowed with such a family. The following PRs will add the definitions of heights of tuples of elements of K and finitely supported maps to K, prove some basic properties, add an instancesof AdmissibleAbsValues for number fields, etc. See the Heights repository. We need a couple of API lemmas, one of which was put in a new file because no suitable existing home could be found.