∀ (p k : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  [hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] (P : Ideal (NumberField.RingOfIntegers K)) [hP₁ : P.IsPrime]
  [hP₂ : P.LiesOver (Ideal.span {↑p})], (Ideal.span {↑p}).ramificationIdx P = p ^ k * (p - 1)