Definitions/Def_NumberField_IsSplitPrime.lean

Fix number fields K and M with M a Galois extension of K. For an ideal \mathfrak{l} of the ring of integers \mathcal{O}_K, the predicate NumberField.IsSplitPrime K M 𝔩 is the conjunction of three conditions. First, \mathfrak{l} is a maximal ideal of \mathcal{O}_K. Second, the absolute norm \operatorname{absNorm} \mathfrak{l}, i.e. the cardinality of \mathcal{O}_K/\mathfrak{l} as a natural number, is a prime number; together with maximality this says exactly that \mathfrak{l} is a prime of K of residue degree one over \mathbb{Q}, with residue field \mathbb{F}_\ell for \ell = \operatorname{absNorm} \mathfrak{l}. Third, the number of primes of \mathcal{O}_M lying over \mathfrak{l}, measured as the Nat.card of Mathlib's set 𝔩.primesOver (𝓞 M) of maximal ideals of \mathcal{O}_M above \mathfrak{l}, equals \operatorname{finrank}_K M = [M:K].

The third clause is thus phrased as a counting condition on the fibre of \operatorname{Spec} \mathcal{O}_M \to \operatorname{Spec} \mathcal{O}_K over \mathfrak{l}, not as the assertion that all ramification indices and residue degrees equal one; in the Galois situation the two are equivalent, since efg = [M:K] forces e = f = 1 precisely when g = [M:K]. So IsSplitPrime K M 𝔩 holds exactly for those degree-one primes of K which split completely in M; its negation, imposed alongside the first two clauses, singles out the degree-one primes of K that are not completely split in M.