Theorems · Theorem · number theory

NumberField.InfinitePlace.even_nat_card_aut_of_not_isUnramified

∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K]
  {w : NumberField.InfinitePlace K} [IsGalois k K],
  ¬NumberField.InfinitePlace.IsUnramified k w → Even (Nat.card Gal(K/k))

Defined in: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
Cited by: 1 results in Mathlib
Foundations: Depth 181 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Field Field Algebra IsGalois

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites17

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Algebrastatement and proof · cited by 11,388
Fintypeproof · cited by 7,736
Fieldstatement and proof · cited by 7,404
Finiteproof · cited by 3,029
AlgEquivstatement and proof · cited by 1,681
Nat.cardstatement and proof · cited by 844
NumberField.InfinitePlacestatement and proof · cited by 604
Evenstatement and proof · cited by 444
nonempty_fintypeproof · cited by 261
MulAction.stabilizerproof · cited by 254
IsGaloisstatement and proof · cited by 149
NumberField.InfinitePlace.IsUnramifiedstatement and proof · cited by 35

Cited by1

Results whose statement or proof uses this declaration.

NumberField.InfinitePlace.even_card_aut_of_not_isUnramifiedproof · cited by 3