Commit 2026-03-06 11:44 7f31b369

feat(NumberTheory/Height/MvPolynomial): new file (#35925) We add a module Mathlib.NumberTheory.Height.MvPolynomial, whose contents are meant to be about height bounds for the image of a polynomial map between projective spaces with given basis, expressed in terms of coordinate tuples. This first instalment contains upper bounds for linea maps; upper and lower bounds for polynomial maps will follow.