English
If p is maximal and K/L is a Galois extension, the inertia degrees over p for P and Q lying over p are equal: inertiaDeg p P = inertiaDeg p Q.
Русский
Если p максимален и K/L Галуа-расширение, то инерциальные степени над p для P и Q, лежащих над p, равны: inertiaDeg p P = inertiaDeg p Q.
LaTeX
$$$\\mathrm{inertiaDeg}_p(p\\; B)\\; P = \\mathrm{inertiaDeg}_p(p\\; B)\\; Q$$$
Lean4
/-- All the `inertiaDeg` over a fixed maximal ideal are the same. -/
theorem inertiaDeg_eq_of_isGalois [p.IsMaximal] [IsGalois K L] : inertiaDeg p P = inertiaDeg p Q :=
by
rcases exists_map_eq_of_isGalois p P Q K L with ⟨σ, hs⟩
rw [← hs]
exact (inertiaDeg_map_eq p P σ).symm