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₁]
:
A field that satisfies the Northcott property for mulHeight₁ also does for logHeight₁.