inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply'

English

The inertia degree of the prime over p corresponding to Q equals the degree of Q modulo p.

Русский

Направленный над p простейший идеал имеет инерционную степень, равную степенy Q мод p.

LaTeX

$$inertiaDeg (span {p}) ((primesOverSpanEquivMonicFactorsMod hp).symm ⟨Q.map (Int.castRingHom (ZMod p)), hQ⟩ : Ideal (𝓞_K)) = natDegree (Q.map (Int.castRingHom (ZMod p)))$$

Lean4

theorem inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply' (hp : ¬p ∣ exponent θ) {Q : (ZMod p)[X]}
    (hQ : Q ∈ monicFactorsMod θ p) :
    inertiaDeg (span {(p : ℤ)}) ((primesOverSpanEquivMonicFactorsMod hp).symm ⟨Q, hQ⟩ : Ideal (𝓞 K)) = natDegree Q :=
  by
  obtain ⟨S, rfl⟩ := (map_surjective _ (ZMod.ringHom_surjective (Int.castRingHom (ZMod p)))) Q
  rw [inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply]

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