Theorems · Theorem · number theory

NumberField.InfinitePlace.card_eq_card_isUnramifiedIn

∀ (k : Type u_1) [inst : Field k] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra k K] [inst_3 : NumberField K]
  [inst_4 : NumberField k] [IsGalois k K],
  Fintype.card (NumberField.InfinitePlace K) =
    {w | NumberField.InfinitePlace.IsUnramifiedIn K w}.card * Module.finrank k K +
      {w | NumberField.InfinitePlace.IsUnramifiedIn K w}ᶜ.card * (Module.finrank k K / 2)

Defined in

Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Cited by

1 results in Mathlib

Foundations

Depth 300 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldFieldAlgebraNumberFieldNumberFieldIsGalois