Structures · Order
Northcott
A function h : α → β is Northcott if the sets {a : α | h a ≤ b} are all finite.
- Defined in
- Mathlib.Order.Northcott
- Shape
- One type argument · adds finite_le
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- IsDedekindDomain.HeightOneSpectrum
- Ideal
How is a type an instance?
Loading the hierarchy index…
Assumed by18
- Northcott.finite_le
- Northcott.exists_min_image
- CommGroup.fg_of_descent
- Monoid.finite_set_isOfFiniteOrder_of_descent
- AddMonoid.finite_set_isOfFiniteOrder_of_descent
- AddCommGroup.finite_torsion_of_descent
- AddGroup.fg_of_descent
- Group.fg_of_descent
- AddCommGroup.fg_of_descent
- CommGroup.finite_torsion_of_descent
- AddCommGroup.fg_of_descent'
- CommGroup.fg_of_descent'
- Northcott.comp_of_bddAbove
- Northcott.comp_of_finite_fibers
- Height.instNorthcottRealLogHeight₁OfMulHeight₁
- CommGroup.finite_torsion_of_descent'
- AddCommGroup.finite_torsion_of_descent'
- ArithmeticFunction.tendsTo_eulerProduct_ofPowerSeries
Ancestors0
No ancestors.