isUnramified_iff_stabilizer_eq_bot

English

For IsGalois, IsUnramified k w is equivalent to the stabilizer of w being trivial.

Русский

Для IsGalois эквивалентно: неразм.

LaTeX

$$$IsUnramified\\; k\\; w \\iff Stab w = \\{1\\}$$$

Lean4

theorem isUnramified_iff_stabilizer_eq_bot [IsGalois k K] : IsUnramified k w ↔ Stab w = ⊥ :=
  by
  rw [← mk_embedding w, isUnramified_mk_iff_forall_isConj]
  simp only [eq_bot_iff, SetLike.le_def, mem_stabilizer_mk_iff, Subgroup.mem_bot, forall_eq_or_imp, true_and]

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