English
The ramification index for the symmetric image equals the multiplicity of the image of Q modulo p in minpoly modulo p.
Русский
Рамификационное разветвление для симметрического образа равно кратности образа Q по модулю p в минимальном полиноме по модулю p.
LaTeX
$$ramificationIdx (algebraMap Z (𝓞_K)) (span {p : Z}) ((primesOverSpanEquivMonicFactorsMod hp).symm ⟨Q.map (Int.castRingHom (ZMod p)), hQ⟩ : Ideal (𝓞_K)) = multiplicity (Q.map (Int.castRingHom (ZMod p))) ((minpoly Z θ).map (Int.castRingHom (ZMod p)))$$
Lean4
theorem ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply' (hp : ¬p ∣ exponent θ) {Q : (ZMod p)[X]}
(hQ : Q ∈ monicFactorsMod θ p) :
ramificationIdx (algebraMap ℤ (𝓞 K)) (span {(p : ℤ)})
((primesOverSpanEquivMonicFactorsMod hp).symm ⟨Q, hQ⟩ : Ideal (𝓞 K)) =
multiplicity Q ((minpoly ℤ θ).map (Int.castRingHom (ZMod p))) :=
by
obtain ⟨S, rfl⟩ := (map_surjective _ (ZMod.ringHom_surjective (Int.castRingHom (ZMod p)))) Q
rw [ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply]
