obtain ⟨i, Hi⟩ := hf
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : Fact (↑p).Prime
ζ : 𝓞 L
hζ : IsPrimitiveRoot ζ ↑p
f : Fin ↑p → ℤ
hf : ∃ i, f i = 0
m : ℤ
hdiv : ↑m ∣ ∑ j : Fin ↑p, f j • ζ ^ ↑j
⊢ m ∣ f ⟨(↑p).pred, ⋯⟩
case intro
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : Fact (↑p).Prime
ζ : 𝓞 L
hζ : IsPrimitiveRoot ζ ↑p
f : Fin ↑p → ℤ
m : ℤ
hdiv : ↑m ∣ ∑ j : Fin ↑p, f j • ζ ^ ↑j
i : Fin ↑p
Hi : f i = 0
⊢ m ∣ f ⟨(↑p).pred, ⋯⟩