4. Chebotarev: cyclotomic case🔗

For a cyclotomic extension L = K(\zeta_m), Chebotarev's theorem reduces directly to Dirichlet's argument. Source: Sharifi 7.2.1 (pp. 142--143).

Lemma4.1

uses 1used by 0✓L∃∀N

Let L = K(\zeta_m), \mathfrak{p} a nonzero prime of \mathcal{O}_K unramified in L, and \mathfrak{P} a prime of \mathcal{O}_L above \mathfrak{p}. Then for every primitive m-th root of unity \zeta \in L, \Frob_\mathfrak{P}(\zeta) \;=\; \zeta^{\Norm\mathfrak{p}}.

Definition 2.4

Lean code for Lemma4.1●1 theorem

theoremdefined in CebotarevDensity/CyclotomicNormResidue.lean

complete

theorem Chebotarev.cyclotomic_frobenius_acts_as_norm_power.{u_1, u_2}
  (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L]
  [NumberField L] [Algebra K L] [IsGalois K L] (m : ℕ) [NeZero m]
  [IsCyclotomicExtension {m} K L]
  (𝔭 : Ideal (NumberField.RingOfIntegers K)) [𝔭.IsPrime]
  (hunr : Chebotarev.UnramifiedIn K L 𝔭)
  (hcop : (Ideal.absNorm 𝔭).Coprime m)
  (𝔓 : Ideal (NumberField.RingOfIntegers L)) [𝔓.IsPrime]
  (hP : 𝔓.LiesOver 𝔭) (ζ : L) :
  ζ ∈ primitiveRoots m L →
    (arithFrobAt (NumberField.RingOfIntegers K) Gal(L/K) 𝔓) ζ =
      ζ ^ Ideal.absNorm 𝔭

theorem Chebotarev.cyclotomic_frobenius_acts_as_norm_power.{u_1,
    u_2}
  (K : Type u_1) (L : Type u_2) [Field K]
  [NumberField K] [Field L]
  [NumberField L] [Algebra K L]
  [IsGalois K L] (m : ℕ) [NeZero m]
  [IsCyclotomicExtension {m} K L]
  (𝔭 :
    Ideal (NumberField.RingOfIntegers K))
  [𝔭.IsPrime]
  (hunr : Chebotarev.UnramifiedIn K L 𝔭)
  (hcop : (Ideal.absNorm 𝔭).Coprime m)
  (𝔓 :
    Ideal (NumberField.RingOfIntegers L))
  [𝔓.IsPrime] (hP : 𝔓.LiesOver 𝔭)
  (ζ : L) :
  ζ ∈ primitiveRoots m L →
    (arithFrobAt
          (NumberField.RingOfIntegers K)
          Gal(L/K) 𝔓)
        ζ =
      ζ ^ Ideal.absNorm 𝔭

Sharifi 7.2.1 step (i) — cyclotomic Frobenius formula (p. 142).
Verbatim source quote: "we have φ_𝔭(ζ_m) = ζ_m^{N𝔭} for a primitive mth root of
unity ζ_m". The coprimality `hcop : (N𝔭).Coprime m` is Sharifi's implicit
hypothesis made explicit — it is genuinely necessary: if `μ_m ⊆ K` then `L = K`,
`φ_𝔭 = id`, and *every* prime is unramified, yet the formula would force
`N𝔭 ≡ 1 (mod m)`. For a nontrivial extension it is the statement that an
unramified prime does not divide `m`; mathlib currently provides that only over
`ℚ` (`IsCyclotomicExtension.Rat.*`), so over a general base `K` the caller
supplies the coprimality.

(Relocated here from `Cyclotomic.lean` so that `ZetaProduct.lean` — which `Cyclotomic.lean`
imports — can consume it without an import cycle.)

Proof for Lemma 4.1

uses 0

By the defining property of \Frob_\mathfrak{P} (it acts as the \Norm\mathfrak{p}-power map on \mathcal{O}_L/\mathfrak{P}) combined with the fact that \zeta_m lifts isomorphically from the residue field for \mathfrak{p} \nmid m.

Lemma4.2

Statement uses 2

Statement dependency previews

Preview

Definition 2.5

Loading preview

Statement dependency preview content is loaded from the Blueprint HTML cache.

used by 1✓L∃∀N

For every character \chi of G, the partial sum \sum_\mathfrak{p} \chi(\Frob_\mathfrak{p})\, \Norm\mathfrak{p}^{-s} over \mathfrak{p} unramified in L is bounded by C\log(1/(s-1)) + C for some constant C, in a right neighbourhood of s = 1.

Theorem 3.7 Definition 2.5

Lean code for Lemma4.2●1 theorem

theoremdefined in CebotarevDensity/Cyclotomic.lean

complete

theorem Chebotarev.log_artinLSeries_asymp_character_sum.{u_3, u_4}
  (K : Type u_3) (L : Type u_4) [Field K] [NumberField K] [Field L]
  [NumberField L] [Algebra K L] [IsGalois K L]
  [IsMulCommutative Gal(L/K)] (χ : Chebotarev.galoisCharacter K L) :
  ∃ C,
    ∀ᶠ (s : ℝ) in nhdsWithin 1 (Set.Ioi 1),
      ‖∑' (𝔭 : { 𝔭 // 𝔭.IsPrime ∧ Chebotarev.UnramifiedIn K L 𝔭 }),
            ↑(χ (Quotient.out (Chebotarev.frobeniusClass K L ↑𝔭))) *
              ↑(Ideal.absNorm ↑𝔭) ^ (-↑s)‖ ≤
        C * Real.log (1 / (s - 1)) + C

theorem Chebotarev.log_artinLSeries_asymp_character_sum.{u_3,
    u_4}
  (K : Type u_3) (L : Type u_4) [Field K]
  [NumberField K] [Field L]
  [NumberField L] [Algebra K L]
  [IsGalois K L]
  [IsMulCommutative Gal(L/K)]
  (χ : Chebotarev.galoisCharacter K L) :
  ∃ C,
    ∀ᶠ (s : ℝ) in
      nhdsWithin 1 (Set.Ioi 1),
      ‖∑' (𝔭 :
            { 𝔭 //
              𝔭.IsPrime ∧
                Chebotarev.UnramifiedIn K
                  L 𝔭 }),
            ↑(χ
                  (Quotient.out
                    (Chebotarev.frobeniusClass
                      K L ↑𝔭))) *
              ↑(Ideal.absNorm ↑𝔭) ^
                (-↑s)‖ ≤
        C * Real.log (1 / (s - 1)) + C

Sharifi 7.2.1 step (ii) — log of an Artin L-function on the
half-plane `Re s > 1` (p. 142). Verbatim source quote: "log L(χ,s) ~
Σ_𝔭 χ(𝔭) N𝔭^{-s} for Re(s) > 1".

Proof for Lemma 4.2

uses 0

Expand \log L(\chi, s) via the Euler product Lemma 3.2; the higher-power tail is bounded analogously to Lemma 1.2.

Lemma4.3

Statement uses 2

Statement dependency previews

Preview

Definition 2.5

Loading preview

Statement dependency preview content is loaded from the Blueprint HTML cache.

used by 1✓L∃∀N

Let L = K(\zeta_m), \sigma \in G, and \mathfrak{p} a nonzero prime of \mathcal{O}_K unramified in L with \sigma_\mathfrak{p} the conjugacy class of \sigma. Then \sum_{\chi \in \widehat{G}} \chi(\sigma)\, \chi(\Frob_\mathfrak{p})^{-1} \;=\; |G|.

Definition 3.1 Definition 2.5

Lean code for Lemma4.3●1 theorem

theoremdefined in CebotarevDensity/Cyclotomic.lean

complete

theorem Chebotarev.character_orthogonality_cyclotomic_eq.{u_3, u_4}
  (K : Type u_3) (L : Type u_4) [Field K] [NumberField K] [Field L]
  [NumberField L] [Algebra K L] [IsGalois K L] (m : ℕ) [NeZero m]
  [IsCyclotomicExtension {m} K L]
  [Fintype (Chebotarev.galoisCharacter K L)] (σ : Gal(L/K))
  (𝔭 : Ideal (NumberField.RingOfIntegers K)) [𝔭.IsPrime]
  (_hunr : Chebotarev.UnramifiedIn K L 𝔭)
  (_h : Chebotarev.frobeniusClass K L 𝔭 = ConjClasses.mk σ) :
  ∑ χ,
      ↑(χ σ) *
        (↑(χ (Quotient.out (Chebotarev.frobeniusClass K L 𝔭))))⁻¹ =
    ↑(Nat.card Gal(L/K))

theorem Chebotarev.character_orthogonality_cyclotomic_eq.{u_3,
    u_4}
  (K : Type u_3) (L : Type u_4) [Field K]
  [NumberField K] [Field L]
  [NumberField L] [Algebra K L]
  [IsGalois K L] (m : ℕ) [NeZero m]
  [IsCyclotomicExtension {m} K L]
  [Fintype
      (Chebotarev.galoisCharacter K L)]
  (σ : Gal(L/K))
  (𝔭 :
    Ideal (NumberField.RingOfIntegers K))
  [𝔭.IsPrime]
  (_hunr : Chebotarev.UnramifiedIn K L 𝔭)
  (_h :
    Chebotarev.frobeniusClass K L 𝔭 =
      ConjClasses.mk σ) :
  ∑ χ,
      ↑(χ σ) *
        (↑(χ
              (Quotient.out
                (Chebotarev.frobeniusClass
                  K L 𝔭))))⁻¹ =
    ↑(Nat.card Gal(L/K))

Sharifi 7.2.1 step (iii) — character orthogonality for the cyclotomic
case (p. 142), **matching case**: when `frobeniusClass K L 𝔭 =
ConjClasses.mk σ`, the character sum equals `|G|`.

Lemma4.4

Statement uses 2

Statement dependency previews

Preview

Definition 2.5

Loading preview

Statement dependency preview content is loaded from the Blueprint HTML cache.

used by 1✓L∃∀N

Let L = K(\zeta_m), \sigma \in G, and \mathfrak{p} a nonzero prime of \mathcal{O}_K unramified in L whose Frobenius class is not the conjugacy class of \sigma. Then \sum_{\chi \in \widehat{G}} \chi(\sigma)\, \chi(\Frob_\mathfrak{p})^{-1} \;=\; 0.

Definition 3.1 Definition 2.5

Lean code for Lemma4.4●1 theorem

theoremdefined in CebotarevDensity/Cyclotomic.lean

complete

theorem Chebotarev.character_orthogonality_cyclotomic_ne.{u_3, u_4}
  (K : Type u_3) (L : Type u_4) [Field K] [NumberField K] [Field L]
  [NumberField L] [Algebra K L] [IsGalois K L] (m : ℕ) [NeZero m]
  [IsCyclotomicExtension {m} K L]
  [Fintype (Chebotarev.galoisCharacter K L)] (σ : Gal(L/K))
  (𝔭 : Ideal (NumberField.RingOfIntegers K)) [𝔭.IsPrime]
  (_hunr : Chebotarev.UnramifiedIn K L 𝔭)
  (_h : Chebotarev.frobeniusClass K L 𝔭 ≠ ConjClasses.mk σ) :
  ∑ χ,
      ↑(χ σ) *
        (↑(χ (Quotient.out (Chebotarev.frobeniusClass K L 𝔭))))⁻¹ =
    0

theorem Chebotarev.character_orthogonality_cyclotomic_ne.{u_3,
    u_4}
  (K : Type u_3) (L : Type u_4) [Field K]
  [NumberField K] [Field L]
  [NumberField L] [Algebra K L]
  [IsGalois K L] (m : ℕ) [NeZero m]
  [IsCyclotomicExtension {m} K L]
  [Fintype
      (Chebotarev.galoisCharacter K L)]
  (σ : Gal(L/K))
  (𝔭 :
    Ideal (NumberField.RingOfIntegers K))
  [𝔭.IsPrime]
  (_hunr : Chebotarev.UnramifiedIn K L 𝔭)
  (_h :
    Chebotarev.frobeniusClass K L 𝔭 ≠
      ConjClasses.mk σ) :
  ∑ χ,
      ↑(χ σ) *
        (↑(χ
              (Quotient.out
                (Chebotarev.frobeniusClass
                  K L 𝔭))))⁻¹ =
    0

Sharifi 7.2.1 character orthogonality, **non-matching case**:
when `frobeniusClass K L 𝔭 ≠ ConjClasses.mk σ`, the character sum
vanishes.

Proof for Lemma 4.4

uses 0

Standard finite-group character orthogonality for the dual of G (Sharifi 7.2.1 step at p. 142). Under the isomorphism G \cong (\mathbb{Z}/m\mathbb{Z})^\times from Lemma 4.1, \chi(\Frob_\mathfrak{p}) depends only on \Norm\mathfrak{p} \bmod m, and the sum reduces to the orthogonality relation on the cyclic group (\mathbb{Z}/m\mathbb{Z})^\times.

Lemma4.5

Statement uses 4

Statement dependency previews

Preview

Lemma 3.6

Loading preview

Statement dependency preview content is loaded from the Blueprint HTML cache.

used by 1✓L∃∀N

Let L = K(\zeta_m) and \sigma \in G. The Frobenius-fibre prime sum is asymptotic to (1/|G|)\log(1/(s-1)): \lim_{s \downarrow 1} \frac{\sum_{\mathfrak{p}:\, \sigma_\mathfrak{p} = \sigma} \Norm\mathfrak{p}^{-s}}{\log(1/(s-1))} \;=\; \frac{1}{|G|}.

Lemma 4.2 Lemma 4.3 Lemma 4.4 Lemma 3.6

Lean code for Lemma4.5●1 theorem

theoremdefined in CebotarevDensity/Cyclotomic.lean

complete

theorem Chebotarev.primeIdealZetaSum_frobeniusFibre_asymp.{u_3, u_4}
  (K : Type u_3) (L : Type u_4) [Field K] [NumberField K] [Field L]
  [NumberField L] [Algebra K L] [IsGalois K L] (m : ℕ) [NeZero m]
  [IsCyclotomicExtension {m} K L] (hm : m % 4 ≠ 2) (σ : Gal(L/K)) :
  Filter.Tendsto
    (fun s ↦
      Chebotarev.primeIdealZetaSum
          {𝔭 |
            𝔭.IsPrime ∧
              Chebotarev.UnramifiedIn K L 𝔭 ∧
                Chebotarev.frobeniusClass K L 𝔭 = ConjClasses.mk σ}
          s /
        Real.log (1 / (s - 1)))
    (nhdsWithin 1 (Set.Ioi 1)) (nhds (↑(Nat.card Gal(L/K)))⁻¹)

theorem Chebotarev.primeIdealZetaSum_frobeniusFibre_asymp.{u_3,
    u_4}
  (K : Type u_3) (L : Type u_4) [Field K]
  [NumberField K] [Field L]
  [NumberField L] [Algebra K L]
  [IsGalois K L] (m : ℕ) [NeZero m]
  [IsCyclotomicExtension {m} K L]
  (hm : m % 4 ≠ 2) (σ : Gal(L/K)) :
  Filter.Tendsto
    (fun s ↦
      Chebotarev.primeIdealZetaSum
          {𝔭 |
            𝔭.IsPrime ∧
              Chebotarev.UnramifiedIn K L
                  𝔭 ∧
                Chebotarev.frobeniusClass
                    K L 𝔭 =
                  ConjClasses.mk σ}
          s /
        Real.log (1 / (s - 1)))
    (nhdsWithin 1 (Set.Ioi 1))
    (nhds (↑(Nat.card Gal(L/K)))⁻¹)

Sharifi 7.2.1 step (iv-a) — the numerator asymptotic. The prime-sum over the Frobenius fibre
`{σ_𝔭 = σ}` is asymptotic to `(1/|G|) log(1/(s-1))` as `s ↓ 1`.

Proof for Lemma 4.5

Proof uses 3

Proof dependency previews

Preview

Lemma 3.6

Loading preview

Proof dependency preview content is loaded from the Blueprint HTML cache.

Multiply \log L(\chi, s) by \chi(\sigma)^{-1} and sum over \chi: the orthogonality relations (Lemma 4.3 and Lemma 4.4) pick out the primes with Frobenius \sigma, giving \sum_\chi \chi(\sigma)^{-1}\log L(\chi, s) \sim |G| \sum_{\sigma_\mathfrak{p} = \sigma} \Norm\mathfrak{p}^{-s}; on the other hand it is \sim \log\zeta_K(s) \sim \log(1/(s-1)) (only \chi = \mathbf{1} contributes a pole, by Lemma 3.6). Divide.

Lemma 4.3 Lemma 4.4 Lemma 3.6

Lemma4.6

uses 0used by 1✓L∃∀N

If \operatorname{num}(s)/\log(1/(s-1)) \to c and \operatorname{den}(s)/\log(1/(s-1)) \to 1 as s \downarrow 1, then \operatorname{num}(s)/\operatorname{den}(s) \to c.

Lean code for Lemma4.6●1 theorem

theoremdefined in CebotarevDensity/Cyclotomic.lean

complete

theorem Chebotarev.tendsto_ratio_of_log_asymp_numerator (num den : ℝ → ℝ)
  (c : ℝ)
  (hnum :
    Filter.Tendsto (fun s ↦ num s / Real.log (1 / (s - 1)))
      (nhdsWithin 1 (Set.Ioi 1)) (nhds c))
  (hden :
    Filter.Tendsto (fun s ↦ den s / Real.log (1 / (s - 1)))
      (nhdsWithin 1 (Set.Ioi 1)) (nhds 1)) :
  Filter.Tendsto (fun s ↦ num s / den s) (nhdsWithin 1 (Set.Ioi 1))
    (nhds c)

theorem Chebotarev.tendsto_ratio_of_log_asymp_numerator
  (num den : ℝ → ℝ) (c : ℝ)
  (hnum :
    Filter.Tendsto
      (fun s ↦
        num s / Real.log (1 / (s - 1)))
      (nhdsWithin 1 (Set.Ioi 1)) (nhds c))
  (hden :
    Filter.Tendsto
      (fun s ↦
        den s / Real.log (1 / (s - 1)))
      (nhdsWithin 1 (Set.Ioi 1))
      (nhds 1)) :
  Filter.Tendsto (fun s ↦ num s / den s)
    (nhdsWithin 1 (Set.Ioi 1)) (nhds c)

Pure real-analysis glue: if `num(s) / log(1/(s-1)) → c` and
`den(s) / log(1/(s-1)) → 1` as `s ↓ 1`, then `num(s) / den(s) → c`.

Proof for Lemma 4.6

uses 0

Write \operatorname{num}/\operatorname{den} = (\operatorname{num}/L)/(\operatorname{den}/L) with L = \log(1/(s-1)), which is positive (hence nonzero) for s \in (1,2) since 1/(s-1) > 1; apply the quotient rule for limits and cancel L.

Lemma4.7

Statement uses 3

Statement dependency previews

Preview

Lemma 1.8

Loading preview

Statement dependency preview content is loaded from the Blueprint HTML cache.

used by 1✓L∃∀N

Let L = K(\zeta_m) and \sigma \in G. Then \lim_{s \downarrow 1} \frac{\sum_{\mathfrak{p}:\, \sigma_\mathfrak{p} = \sigma} \Norm\mathfrak{p}^{-s}}{\sum_\mathfrak{p} \Norm\mathfrak{p}^{-s}} \;=\; \frac{1}{|G|}.

Lemma 4.5 Lemma 1.8 Lemma 4.6

Lean code for Lemma4.7●1 theorem

theoremdefined in CebotarevDensity/Cyclotomic.lean

complete

theorem Chebotarev.cyclotomic_density_from_two_sided_asymp.{u_3, u_4}
  (K : Type u_3) (L : Type u_4) [Field K] [NumberField K] [Field L]
  [NumberField L] [Algebra K L] [IsGalois K L] (m : ℕ) [NeZero m]
  [IsCyclotomicExtension {m} K L] (hm : m % 4 ≠ 2) (σ : Gal(L/K)) :
  Filter.Tendsto
    (fun s ↦
      Chebotarev.primeIdealZetaSum
          {𝔭 |
            𝔭.IsPrime ∧
              Chebotarev.UnramifiedIn K L 𝔭 ∧
                Chebotarev.frobeniusClass K L 𝔭 = ConjClasses.mk σ}
          s /
        Chebotarev.primeIdealZetaSum Set.univ s)
    (nhdsWithin 1 (Set.Ioi 1)) (nhds (↑(Nat.card Gal(L/K)))⁻¹)

theorem Chebotarev.cyclotomic_density_from_two_sided_asymp.{u_3,
    u_4}
  (K : Type u_3) (L : Type u_4) [Field K]
  [NumberField K] [Field L]
  [NumberField L] [Algebra K L]
  [IsGalois K L] (m : ℕ) [NeZero m]
  [IsCyclotomicExtension {m} K L]
  (hm : m % 4 ≠ 2) (σ : Gal(L/K)) :
  Filter.Tendsto
    (fun s ↦
      Chebotarev.primeIdealZetaSum
          {𝔭 |
            𝔭.IsPrime ∧
              Chebotarev.UnramifiedIn K L
                  𝔭 ∧
                Chebotarev.frobeniusClass
                    K L 𝔭 =
                  ConjClasses.mk σ}
          s /
        Chebotarev.primeIdealZetaSum
          Set.univ s)
    (nhdsWithin 1 (Set.Ioi 1))
    (nhds (↑(Nat.card Gal(L/K)))⁻¹)

Sharifi 7.2.1 step (iv) — two-sided log-asymptotic comparison (p. 142).
Source: "on the one hand we have Σ_χ χ(σ)^{-1} log L(χ,s) ~ |G|
Σ_{φ_𝔭=σ} N𝔭^{-s}, whereas on the other we have Σ_χ χ(σ)^{-1} log L(χ,s)
~ log ζ_K(s) ~ log(s-1)^{-1}". Comparing yields density `1/|G|`.

Proof for Lemma 4.7

Proof uses 3

Proof dependency previews

Preview

Lemma 1.8

Loading preview

Proof dependency preview content is loaded from the Blueprint HTML cache.

The numerator asymptotic Lemma 4.5 (\operatorname{num} \sim (1/|G|)\log(1/(s-1))) and the denominator asymptotic Lemma 1.8 (\operatorname{den} \sim \log(1/(s-1))) feed the ratio glue Lemma 4.6.

Lemma 4.5 Lemma 1.8 Lemma 4.6

Theorem4.8

Statement uses 3

Statement dependency previews

Preview

Definition 1.1

Loading preview

Statement dependency preview content is loaded from the Blueprint HTML cache.

used by 1✓L∃∀N

For K a number field, m \ge 1, L = K(\zeta_m), and every \sigma \in G = \Gal{L/K}, \delta\bigl(\{\mathfrak{p} \subset \mathcal{O}_K : \sigma_\mathfrak{p} = \sigma\}\bigr) \;=\; \frac{1}{|G|}.

Definition 1.1 Definition 2.5 Lemma 4.7

Lean code for Theorem4.8●1 theorem

theoremdefined in CebotarevDensity/Cyclotomic.lean

complete

theorem Chebotarev.chebotarev_cyclotomic.{u_1, u_2} (K : Type u_1)
  (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L]
  [Algebra K L] [IsGalois K L] (m : ℕ) [NeZero m]
  [IsCyclotomicExtension {m} K L] (hm : m % 4 ≠ 2) (σ : Gal(L/K)) :
  Chebotarev.HasDirichletDensity
    {𝔭 |
      𝔭.IsPrime ∧
        Chebotarev.UnramifiedIn K L 𝔭 ∧
          Chebotarev.frobeniusClass K L 𝔭 = ConjClasses.mk σ}
    (↑(Nat.card Gal(L/K)))⁻¹

theorem Chebotarev.chebotarev_cyclotomic.{u_1,
    u_2}
  (K : Type u_1) (L : Type u_2) [Field K]
  [NumberField K] [Field L]
  [NumberField L] [Algebra K L]
  [IsGalois K L] (m : ℕ) [NeZero m]
  [IsCyclotomicExtension {m} K L]
  (hm : m % 4 ≠ 2) (σ : Gal(L/K)) :
  Chebotarev.HasDirichletDensity
    {𝔭 |
      𝔭.IsPrime ∧
        Chebotarev.UnramifiedIn K L 𝔭 ∧
          Chebotarev.frobeniusClass K L
              𝔭 =
            ConjClasses.mk σ}
    (↑(Nat.card Gal(L/K)))⁻¹

**Chebotarev's theorem, cyclotomic case** (Sharifi §7.2.1).

For `K` a number field, `m ≥ 1`, and `L = K(μ_m)` the `m`-th cyclotomic
extension of `K`, every `σ ∈ Gal(L/K)` is the Frobenius of a set of primes
of `𝓞 K` (unramified in `L`) of Dirichlet density `1 / |Gal(L/K)|`.