ClassFieldTheory.FinitePrimeSplitsCompletely
A finite prime splits completely when every prime above it has ramification index and inertia degree equal to one.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
namespace ClassFieldTheory
universe u vLean source · statement
def FinitePrimeSplitsCompletely
(K : Type u) (L : Type v)
[Field K] [NumberField K]
[Field L] [NumberField L] [Algebra K L]
(v : HeightOneSpectrum (𝓞 K)) : Prop