Commit 2026-04-27 19:30 0040fde4
View on Github →feat(NumberTheory/Height/NumberField): results on heights over the rational numbers (#38183) This adds the statement that the height of a tuple of coprime integers (considered as rational numbers) is the maximum of their absolute values and also the fact that the height of a rational number is the maximum of the absolute value of its numerator and its denominator. We use this to golf the proof of the statement for natural numbers recently introduced in [#38125](https://github.com/leanprover-community/mathlib4/pull/38125).