ramificationIdx_ne_zero — Mathlib

English

If p ≠ ⊥ and map f p ≤ P with P prime, then the ramification index e over p to P is nonzero.

Русский

Если p ≠ ⊥ и map f p ≤ P при Pprime, то рамфикационный индекс над p не равен нулю.

LaTeX

$$$\\\\operatorname{ramificationIdx} f p P \\\\neq 0$$$

Lean4

theorem ramificationIdx_ne_zero (hp0 : map f p ≠ ⊥) (hP : P.IsPrime) (le : map f p ≤ P) : ramificationIdx f p P ≠ 0 :=
  by
  classical
  have hP0 : P ≠ ⊥ := by
    rintro rfl
    exact hp0 (le_bot_iff.mp le)
  have hPirr := (Ideal.prime_of_isPrime hP0 hP).irreducible
  rw [IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count hp0 hP hP0]
  obtain ⟨P', hP', P'_eq⟩ := exists_mem_normalizedFactors_of_dvd hp0 hPirr (Ideal.dvd_iff_le.mpr le)
  rwa [Multiset.count_ne_zero, associated_iff_eq.mp P'_eq]

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