not_isUnramified_iff_card_stabilizer_eq_two

English

Not unramified iff the stabilizer has size 2 (under Galois).

Русский

Неразм. если стабилизатор имеет размер 2 (при Galois).

LaTeX

$$$\\neg IsUnramified\\; k\\; w \\iff Nat.card(Stab w) = 2$$$

Lean4

theorem not_isUnramified_iff_card_stabilizer_eq_two [IsGalois k K] : ¬IsUnramified k w ↔ Nat.card (Stab w) = 2 :=
  by
  rw [isUnramified_iff_card_stabilizer_eq_one]
  obtain (e | e) := nat_card_stabilizer_eq_one_or_two k w <;> rw [e] <;> decide

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