even_finrank_of_not_isUnramifiedIn

English

If [IsGalois k K] and w.IsUnramifiedIn K is false, then finrank k K is even.

Русский

Если расширение галое k ⊆ K и w.IsUnramifiedIn K ложно, то финразмерность $[K:k]$ чётна.

LaTeX

$$If [IsGalois k K] and ¬ w.IsUnramifiedIn K, then Even (finrank k K).$$

Lean4

theorem even_finrank_of_not_isUnramifiedIn [IsGalois k K] {w : InfinitePlace k} (hw : ¬w.IsUnramifiedIn K) :
    Even (finrank k K) := by
  obtain ⟨v, rfl⟩ := comap_surjective (K := K) w
  rw [isUnramifiedIn_comap] at hw
  exact even_finrank_of_not_isUnramified hw

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