ramificationIdx_eq_normalizedFactors_count

English

Under localization, ramificationIdx coincides with the count of normalized factors at P.

Русский

При локализации ramificationIdx совпадает с числом нормализованных факторов при P.

LaTeX

$$$ramificationIdx f p P = (normalizedFactors (map f p)).count P$$$

Lean4

theorem ramificationIdx_eq_normalizedFactors_count [DecidableEq (Ideal S)] (hp0 : map f p ≠ ⊥) (hP : P.IsPrime)
    (hP0 : P ≠ ⊥) : ramificationIdx f p P = (normalizedFactors (map f p)).count P :=
  by
  have hPirr := (Ideal.prime_of_isPrime hP0 hP).irreducible
  refine ramificationIdx_spec (Ideal.le_of_dvd ?_) (mt Ideal.dvd_iff_le.mpr ?_) <;>
    rw [dvd_iff_normalizedFactors_le_normalizedFactors (pow_ne_zero _ hP0) hp0, normalizedFactors_pow,
      normalizedFactors_irreducible hPirr, normalize_eq, Multiset.nsmul_singleton, ← Multiset.le_count_iff_replicate_le]
  exact (Nat.lt_succ_self _).not_ge

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