ramificationIdx_ne_zero_of_liesOver

English

If P lies over p (i.e., P is a prime above p) and p ≠ ⊥, then the ramification index e over p to P is nonzero.

Русский

Если P лежит над p (P выше p) и p ≠ ⊥, то рамificationIdx над p к P не равен нулю.

LaTeX

$$$\\\\operatorname{ramificationIdx} (\\\\text{algebraMap } R S) p P \\\\neq 0$$$

Lean4

theorem ramificationIdx_ne_zero_of_liesOver [Algebra R S] [NoZeroSMulDivisors R S] (P : Ideal S) [hP : P.IsPrime]
    {p : Ideal R} (hp : p ≠ ⊥) [hPp : P.LiesOver p] : ramificationIdx (algebraMap R S) p P ≠ 0 :=
  IsDedekindDomain.ramificationIdx_ne_zero (map_ne_bot_of_ne_bot hp) hP <|
    map_le_iff_le_comap.mpr <| le_of_eq <| (liesOver_iff _ _).mp hPp

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