even_nat_card_aut_of_not_isUnramified

English

If w is not unramified, then the automorphism group size is even (under IsGalois).

Русский

Если w неразморожено, то размер группы автоморфизмов чётный.

LaTeX

$$[IsGalois k K] \\; IsUnramified k w \\Rightarrow \\text{Even}(\\lvert K \\simeq_k K \\rvert)$$

Lean4

theorem even_nat_card_aut_of_not_isUnramified [IsGalois k K] (hw : ¬IsUnramified k w) : Even (Nat.card <| K ≃ₐ[k] K) :=
  by
  by_cases H : Finite (K ≃ₐ[k] K)
  · cases nonempty_fintype (K ≃ₐ[k] K)
    rw [even_iff_two_dvd, ← not_isUnramified_iff_card_stabilizer_eq_two.mp hw]
    exact Subgroup.card_subgroup_dvd_card (Stab w)
  · convert Even.zero
    by_contra e
    exact H (Nat.finite_of_card_ne_zero e)

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