Theorem NumberField.finite_setOf_mulHeight₁_le

Modification history

2026-07-17 09:57

Mathlib/NumberTheory/Height/NumberField.lean

chore(Data): rename `setOf` to `Set.ofPred` (#41507) …

Deleted NumberField.finite_setOf_mulHeight₁_le View on Github →

2026-06-26 12:09

Mathlib/NumberTheory/Height/NumberField.lean

feat(NumberTheory/Height/NumberField): Northcott property (#39744) …

Added NumberField.finite_setOf_mulHeight₁_le View on Github →