Commit 2026-06-26 12:09 cce5343a

View on Github →

feat(NumberTheory/Height/NumberField): Northcott property (#39744) This PR finally adds a proof of the Northcott property for heights on number fields:

theorem NumberField.finite_setOf_mulHeight₁_le (B : ℝ) : {x : K | mulHeight₁ x ≤ B}.Finite

Estimated changes

Modified Mathlib/NumberTheory/Height/NumberField.lean

added theorem NumberField.exists_nat_le_mulHeight₁

added theorem NumberField.exists_nat_ne_zero_exists_integer_mul_eq_and_absNorm_span_eq_pow

added theorem NumberField.finite_setOf_logHeight₁_le

added theorem NumberField.finite_setOf_mulHeight_nat_le

added theorem NumberField.finite_setOf_mulHeight₁_le

added theorem NumberField.finite_setOf_prod_infinitePlace_iSup_le