inertiaDegIn_eq_inertiaDeg — Mathlib

English

For p maximal and IsGalois, inertiaDegIn p B equals inertiaDeg p P for any P lying over p.

Русский

При p максимальном и IsGalois, inertiaDegIn p B = inertiaDeg p P для любого P над p.

LaTeX

$$$\\mathrm{inertiaDegIn}\\ p\\ B = \\mathrm{inertiaDeg}\\ p\\ P$$$

Lean4

/-- The `inertiaDegIn` is equal to any ramification index over the same ideal. -/
theorem inertiaDegIn_eq_inertiaDeg [p.IsMaximal] [IsGalois K L] : inertiaDegIn p B = inertiaDeg p P :=
  by
  have h : ∃ P : Ideal B, P.IsPrime ∧ P.LiesOver p := ⟨P, hPp, hp⟩
  obtain ⟨_, _⟩ := h.choose_spec
  rw [inertiaDegIn, dif_pos h]
  exact inertiaDeg_eq_of_isGalois p h.choose P K L

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