feat(NumberTheory/Height/NumberField): results on heights over the rational numbers

[MichaelStollBayreuth]

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.

---

[github-actions]

PR summary ff517753c5

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.NumberTheory.Height.NumberField	3002	3017	+15 (+0.50%)

Import changes for all files

Files	Import difference
Mathlib.NumberTheory.Height.NumberField	15

---

Declarations diff

+ Finset.gcd_eq_sum_mul
+ iSup_finitePlace_apply_eq_one_of_gcd_eq_one
+ instance : AddGroupSeminormClass (FinitePlace K) K ℝ
+ logHeight_eq_max_abs_of_gcd_eq_one
+ logHeight₁_eq_log_max
+ mulHeight_eq_max_abs_of_gcd_eq_one
+ mulHeight_eq_max_abs_of_gcd_eq_one'
+ mulHeight₁_eq_max
+ prod_infinitePlace

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).