IsUnramifiedAtInfinitePlaces_of_odd_card_aut

English

If w.IsUnramifiedIn K fails, then finrank k K is even; equivalently, odd finrank ensures unramified-in.

Русский

Если wIsUnramifiedIn K ложно, то finrank k K чётно; напротив, нечётная размерность предполагает безразветвленность.

LaTeX

$$If hw : ¬ w.IsUnramifiedIn K, then Even (finrank k K).$$

Lean4

theorem IsUnramifiedAtInfinitePlaces_of_odd_card_aut [IsGalois k K] (h : Odd (Nat.card <| K ≃ₐ[k] K)) :
    IsUnramifiedAtInfinitePlaces k K :=
  ⟨fun _ ↦ not_not.mp (Nat.not_even_iff_odd.2 h ∘ InfinitePlace.even_card_aut_of_not_isUnramified)⟩

Похожие утверждения