Commit 2026-02-18 07:51 777913b9

feat(NumberTheory/Height/Projectivization): new file (#34780) This adds a new file "Mathlib.NumberTheory.Height.Projectivization", which (for now) contains the definition of the multiplicative and logarithmic heights of points in projective space and basic properties of these. The PR also contains extensions for the positivity tactic so that it knows that multiplicative heights are positive and logarithmic heights are nonnegative.