simp only [MulZeroClass.mul_zero, lcm_eq_zero_iff, PNat.ne_zero, or_false_iff] at pdivlcm_h
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h✝ : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
hpl : IsPrimitiveRoot x l
KEY : (lcm l ↑p).totient ≤ (↑p).totient
hirr : Irreducible (cyclotomic ↑p ℚ)
hrank : FiniteDimensional.finrank ℚ K = (↑p).totient
pdivlcm_w : ℕ
pdivlcm_h : lcm l ↑p = ↑p * 0
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
h : pdivlcm_w = 0
⊢ False
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h✝ : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
hpl : IsPrimitiveRoot x l
KEY : (lcm l ↑p).totient ≤ (↑p).totient
hirr : Irreducible (cyclotomic ↑p ℚ)
hrank : FiniteDimensional.finrank ℚ K = (↑p).totient
pdivlcm_w : ℕ
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
h : pdivlcm_w = 0
pdivlcm_h : l = 0
⊢ False