Namespace Height 4 theorems
- Coefficient-height bound for monic factors over a number field
Height.logHeight_coeff_factor_le0 below · cited by 2 · depth 13 - Normalised logarithmic height is invariant under field inclusion
Height.inv_finrank_mul_logHeight_inclusion0 below · cited by 29 · depth 14 - Behaviour of `mulHeightBound` under extension of the base number field
Height.mulHeightBound_map_le1 below · cited by 1 · depth 17 - Logarithmic height multiplies by [L:K] under extension
Height.logHeight_algebraMap0 below · cited by 1 · depth 18