ramificationIdxIn_eq_ramificationIdx

English

For p over A and P a prime of B lying over p, the ramificationIdxIn p B equals ramificationIdx (algebraMap A B) p P.

Русский

Для p над A и простого P в B над p имеет место равенство ramificationIdxIn p B = ramificationIdx (algebraMap A B) p P.

LaTeX

$$$\\mathrm{ramificationIdxIn}\\ p\\ B = \\mathrm{ramificationIdx}(\\mathrm{algebraMap}\\ A B)\\ p\\ P$$$

Lean4

/-- The `ramificationIdxIn` is equal to any ramification index over the same ideal. -/
theorem ramificationIdxIn_eq_ramificationIdx [IsGalois K L] :
    ramificationIdxIn p B = ramificationIdx (algebraMap A B) p P :=
  by
  have h : ∃ P : Ideal B, P.IsPrime ∧ P.LiesOver p := ⟨P, hPp, hp⟩
  obtain ⟨_, _⟩ := h.choose_spec
  rw [ramificationIdxIn, dif_pos h]
  exact ramificationIdx_eq_of_isGalois p h.choose P K L

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