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