exact caseI (Dvd.dvd.mul_left H _)
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
x y z : ℤ
caseI : ¬↑↑p ∣ x * y * z
habs : ↑x + ↑y = 0
H : ↑↑p ∣ z
⊢ False
no goals