IsUnramifiedAtInfinitePlaces_of_odd_finrank

English

If finrank k K is odd, then the extension is unramified at the corresponding infinite places.

Русский

Если finrank k K нечетна, расширение безразветвлено на соответствующих бесконечных местах.

LaTeX

$$If Odd (finrank k K), then IsUnramifiedAtInfinitePlaces k K.$$

Lean4

theorem IsUnramifiedAtInfinitePlaces_of_odd_finrank [IsGalois k K] (h : Odd (Module.finrank k K)) :
    IsUnramifiedAtInfinitePlaces k K :=
  ⟨fun _ ↦ not_not.mp (Nat.not_even_iff_odd.2 h ∘ InfinitePlace.even_finrank_of_not_isUnramified)⟩

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