FLT/NumberField/HeightOneSpectrum.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The height-one spectrum of a number field

Basic countability instances for the height-one spectrum of 𝓞_K, the ring of integers of a number field K.

Imports (4)
Imported by 5 files
  1. instance (instance at line 27) line 27 source
  2. instance (instance at line 30) line 30 source