Results on the Northcott property for heights

Assume that K is a field with a family of admissible absolute values that satisfies the Northcott property for mulHeight₁. We provide instances showing that K also satisfies the Northcott property

• for logHeight₁,
• (TODO) for Projectivization.mulHeight,
• (TODO) for Projectivization.logHeight.

TODO

Add instances for heights on projectivizations.

instance Height.instNorthcottRealLogHeight₁OfMulHeight₁ {K : Type u_1} [Field K] [AdmissibleAbsValues K] [Northcott mulHeight₁] : Northcott logHeight₁

A field that satisfies the Northcott property for mulHeight₁ also does for logHeight₁.