English
If p is a prime ideal in A and lies over in B with IsGalois extension, then ramificationIdxIn p B ≠ 0.
Русский
Если p – простый идеал A и существует Галуа-расширение, то ramificationIdxIn p B ≠ 0.
LaTeX
$$$\\mathrm{ramificationIdxIn\\ } p\\ B \\neq 0$$$
Lean4
theorem ramificationIdxIn_ne_zero [IsDedekindDomain B] {p : Ideal A} [p.IsPrime] (hp : p ≠ ⊥) [IsGalois K L]
[NoZeroSMulDivisors A B] : p.ramificationIdxIn B ≠ 0 :=
by
obtain ⟨P⟩ := (inferInstance : Nonempty (primesOver p B))
rw [ramificationIdxIn_eq_ramificationIdx p P K L]
exact IsDedekindDomain.ramificationIdx_ne_zero_of_liesOver P.1 hp