even_finrank_of_not_isUnramified — Mathlib

English

Let k ⊆ K be a Galois extension of fields. If an infinite place w of K is ramified over k (i.e., not unramified), then the degree [K:k] is even.

Русский

Пусть k ⊆ K будет галлоzовое расширение полей. Если бесконечное место w K разветвлено над k (то есть не безразветвлено), то степень расширения [K:k] чётна.

LaTeX

$$$\\text{If } k \\subseteq K \\text{ is a Galois extension and } w \\in \\mathrm{InfinitePlace}(K) \\text{ with } \\neg \\IsUnramified(k,w), \\text{ then } \\operatorname{finrank}_k K \\text{ is even.}$$$

Lean4

theorem even_finrank_of_not_isUnramified [IsGalois k K] (hw : ¬IsUnramified k w) : Even (finrank k K) :=
  by
  by_cases FiniteDimensional k K
  · exact IsGalois.card_aut_eq_finrank k K ▸ even_card_aut_of_not_isUnramified hw
  · exact finrank_of_not_finite ‹_› ▸ Even.zero

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