Theorem: roots_of_unity_in_cyclo_aux (FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean)

State before:
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
⊢ l ∣ 2 * ↑p
Tactic:
by_contra h
State after:
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
⊢ False

State before:
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
⊢ False
Tactic:
have hpl' : IsPrimitiveRoot (⟨x, hx⟩ : R) l := by
  have nezero : NeZero (l : 𝓞 K) := by
    refine' ⟨fun hzero => _⟩
    simp only [Nat.cast_eq_zero] at hzero
    simp [hzero] at hl
  rw [isRoot_cyclotomic_iff.symm]
  apply hhl
State after:
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
⊢ False

State before:
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
⊢ False
Tactic:
have hpl : IsPrimitiveRoot x l := by
  have : (algebraMap R K) ⟨x, hx⟩ = x := by rfl
  have h4 := IsPrimitiveRoot.map_of_injective hpl' (f := algebraMap (𝓞 K) K); rw [← this]
  apply h4
  apply IsFractionRing.injective
State after:
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
⊢ False

State before:
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
⊢ False
Tactic:
have KEY := contains_two_primitive_roots hpl hζ
State after:
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 ≤ FiniteDimensional.finrank ℚ K
⊢ False

State before:
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 ≤ FiniteDimensional.finrank ℚ K
⊢ False
Tactic:
have hirr : Irreducible (cyclotomic p ℚ) := cyclotomic.irreducible_rat p.prop
State after:
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 ≤ FiniteDimensional.finrank ℚ K
hirr : Irreducible (cyclotomic ↑p ℚ)
⊢ False

State before:
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 ≤ FiniteDimensional.finrank ℚ K
hirr : Irreducible (cyclotomic ↑p ℚ)
⊢ False
Tactic:
have hrank := IsCyclotomicExtension.finrank K hirr
State after:
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 ≤ FiniteDimensional.finrank ℚ K
hirr : Irreducible (cyclotomic ↑p ℚ)
hrank : FiniteDimensional.finrank ℚ K = (↑p).totient
⊢ False

State before:
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 ≤ FiniteDimensional.finrank ℚ K
hirr : Irreducible (cyclotomic ↑p ℚ)
hrank : FiniteDimensional.finrank ℚ K = (↑p).totient
⊢ False
Tactic:
rw [hrank] at KEY
State after:
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
⊢ False

State before:
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
⊢ False
Tactic:
have pdivlcm : (p : ℕ) ∣ lcm l p := dvd_lcm_right l ↑p
State after:
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 : ↑p ∣ lcm l ↑p
⊢ False

State before:
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 : ↑p ∣ lcm l ↑p
⊢ False
Tactic:
cases' pdivlcm with pdivlcm_w pdivlcm_h
State after:
case intro
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 * pdivlcm_w
⊢ False

State before:
case intro
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 * pdivlcm_w
⊢ False
Tactic:
have ineq1 := Nat.totient_super_multiplicative (p : ℕ) pdivlcm_w
State after:
case intro
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 * pdivlcm_w
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (↑p * pdivlcm_w).totient
⊢ False

State before:
case intro
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 * pdivlcm_w
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (↑p * pdivlcm_w).totient
⊢ False
Tactic:
rw [← pdivlcm_h] at ineq1
State after:
case intro
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 * pdivlcm_w
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
⊢ False

State before:
case intro
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 * pdivlcm_w
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
⊢ False
Tactic:
have KEY3 := (mul_le_iff_le_one_right (Nat.totient_pos.2 p.prop)).mp (le_trans ineq1 KEY)
State after:
case intro
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 * pdivlcm_w
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
⊢ False

State before:
case intro
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 * pdivlcm_w
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
⊢ False
Tactic:
have pdiv_ne_zero : 0 < pdivlcm_w := by
  by_contra h
  simp only [not_lt, le_zero_iff] at h
  rw [h] at pdivlcm_h
  simp only [MulZeroClass.mul_zero, lcm_eq_zero_iff, PNat.ne_zero, or_false_iff] at pdivlcm_h
  apply absurd pdivlcm_h (ne_of_gt (Nat.pos_of_mem_divisors hl))
State after:
case intro
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 * pdivlcm_w
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
pdiv_ne_zero : 0 < pdivlcm_w
⊢ False

State before:
case intro
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 * pdivlcm_w
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
pdiv_ne_zero : 0 < pdivlcm_w
⊢ False
Tactic:
have K5 := (Nat.dvd_prime Nat.prime_two).1 (totient_le_one_dvd_two pdiv_ne_zero KEY3)
State after:
case intro
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 * pdivlcm_w
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
pdiv_ne_zero : 0 < pdivlcm_w
K5 : pdivlcm_w = 1 ∨ pdivlcm_w = 2
⊢ False

State before:
case intro
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 * pdivlcm_w
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
pdiv_ne_zero : 0 < pdivlcm_w
K5 : pdivlcm_w = 1 ∨ pdivlcm_w = 2
⊢ False
Tactic:
cases' K5 with K5 K5
State after:
case intro.inl
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 * pdivlcm_w
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
pdiv_ne_zero : 0 < pdivlcm_w
K5 : pdivlcm_w = 1
⊢ False

case intro.inr
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 * pdivlcm_w
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
pdiv_ne_zero : 0 < pdivlcm_w
K5 : pdivlcm_w = 2
⊢ False

State before:
case intro.inl
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 * pdivlcm_w
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
pdiv_ne_zero : 0 < pdivlcm_w
K5 : pdivlcm_w = 1
⊢ False

case intro.inr
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 * pdivlcm_w
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
pdiv_ne_zero : 0 < pdivlcm_w
K5 : pdivlcm_w = 2
⊢ False
Tactic:
rw [K5] at pdivlcm_h
State after:
case intro.inl
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 * 1
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
pdiv_ne_zero : 0 < pdivlcm_w
K5 : pdivlcm_w = 1
⊢ False

case intro.inr
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 * pdivlcm_w
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
pdiv_ne_zero : 0 < pdivlcm_w
K5 : pdivlcm_w = 2
⊢ False

State before:
case intro.inl
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 * 1
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
pdiv_ne_zero : 0 < pdivlcm_w
K5 : pdivlcm_w = 1
⊢ False

case intro.inr
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 * pdivlcm_w
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
pdiv_ne_zero : 0 < pdivlcm_w
K5 : pdivlcm_w = 2
⊢ False
Tactic:
simp only [mul_one] at pdivlcm_h
State after:
case intro.inl
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
pdiv_ne_zero : 0 < pdivlcm_w
K5 : pdivlcm_w = 1
pdivlcm_h : lcm l ↑p = ↑p
⊢ False

case intro.inr
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 * pdivlcm_w
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
pdiv_ne_zero : 0 < pdivlcm_w
K5 : pdivlcm_w = 2
⊢ False

State before:
case intro.inl
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
pdiv_ne_zero : 0 < pdivlcm_w
K5 : pdivlcm_w = 1
pdivlcm_h : lcm l ↑p = ↑p
⊢ False

case intro.inr
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 * pdivlcm_w
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
pdiv_ne_zero : 0 < pdivlcm_w
K5 : pdivlcm_w = 2
⊢ False
Tactic:
rw [lcm_eq_right_iff] at pdivlcm_h
State after:
case intro.inl
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
pdiv_ne_zero : 0 < pdivlcm_w
K5 : pdivlcm_w = 1
pdivlcm_h : l ∣ ↑p
⊢ False

case intro.inl.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 : ℕ
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
pdiv_ne_zero : 0 < pdivlcm_w
K5 : pdivlcm_w = 1
pdivlcm_h : lcm l ↑p = ↑p
⊢ normalize ↑p = ↑p

case intro.inr
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 * pdivlcm_w
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
pdiv_ne_zero : 0 < pdivlcm_w
K5 : pdivlcm_w = 2
⊢ False

State before:
case intro.inl
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
pdiv_ne_zero : 0 < pdivlcm_w
K5 : pdivlcm_w = 1
pdivlcm_h : l ∣ ↑p
⊢ False

case intro.inl.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 : ℕ
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
pdiv_ne_zero : 0 < pdivlcm_w
K5 : pdivlcm_w = 1
pdivlcm_h : lcm l ↑p = ↑p
⊢ normalize ↑p = ↑p

case intro.inr
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 * pdivlcm_w
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
pdiv_ne_zero : 0 < pdivlcm_w
K5 : pdivlcm_w = 2
⊢ False
Tactic:
have K6 : (p : ℕ) ∣ 2 * (p : ℕ) := dvd_mul_left (↑p : ℕ) 2
State after:
case intro.inl
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
pdiv_ne_zero : 0 < pdivlcm_w
K5 : pdivlcm_w = 1
pdivlcm_h : l ∣ ↑p
K6 : ↑p ∣ 2 * ↑p
⊢ False

case intro.inl.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 : ℕ
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
pdiv_ne_zero : 0 < pdivlcm_w
K5 : pdivlcm_w = 1
pdivlcm_h : lcm l ↑p = ↑p
⊢ normalize ↑p = ↑p

case intro.inr
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 * pdivlcm_w
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
pdiv_ne_zero : 0 < pdivlcm_w
K5 : pdivlcm_w = 2
⊢ False

State before:
case intro.inl
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
pdiv_ne_zero : 0 < pdivlcm_w
K5 : pdivlcm_w = 1
pdivlcm_h : l ∣ ↑p
K6 : ↑p ∣ 2 * ↑p
⊢ False

case intro.inl.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 : ℕ
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
pdiv_ne_zero : 0 < pdivlcm_w
K5 : pdivlcm_w = 1
pdivlcm_h : lcm l ↑p = ↑p
⊢ normalize ↑p = ↑p

case intro.inr
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 * pdivlcm_w
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
pdiv_ne_zero : 0 < pdivlcm_w
K5 : pdivlcm_w = 2
⊢ False
Tactic:
apply absurd (dvd_trans pdivlcm_h K6) h
State after:
case intro.inl.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 : ℕ
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
pdiv_ne_zero : 0 < pdivlcm_w
K5 : pdivlcm_w = 1
pdivlcm_h : lcm l ↑p = ↑p
⊢ normalize ↑p = ↑p

case intro.inr
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 * pdivlcm_w
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
pdiv_ne_zero : 0 < pdivlcm_w
K5 : pdivlcm_w = 2
⊢ False

State before:
case intro.inl.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 : ℕ
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
pdiv_ne_zero : 0 < pdivlcm_w
K5 : pdivlcm_w = 1
pdivlcm_h : lcm l ↑p = ↑p
⊢ normalize ↑p = ↑p

case intro.inr
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 * pdivlcm_w
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
pdiv_ne_zero : 0 < pdivlcm_w
K5 : pdivlcm_w = 2
⊢ False
Tactic:
simp only [eq_self_iff_true, normalize_eq, PNat.coe_inj]
State after:
case intro.inr
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 * pdivlcm_w
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
pdiv_ne_zero : 0 < pdivlcm_w
K5 : pdivlcm_w = 2
⊢ False

State before:
case intro.inr
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 * pdivlcm_w
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
pdiv_ne_zero : 0 < pdivlcm_w
K5 : pdivlcm_w = 2
⊢ False
Tactic:
rw [K5] at pdivlcm_h
State after:
case intro.inr
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 * 2
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
pdiv_ne_zero : 0 < pdivlcm_w
K5 : pdivlcm_w = 2
⊢ False

State before:
case intro.inr
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 * 2
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
pdiv_ne_zero : 0 < pdivlcm_w
K5 : pdivlcm_w = 2
⊢ False
Tactic:
rw [mul_comm] at pdivlcm_h
State after:
case intro.inr
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 = 2 * ↑p
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
pdiv_ne_zero : 0 < pdivlcm_w
K5 : pdivlcm_w = 2
⊢ False

State before:
case intro.inr
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 = 2 * ↑p
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
pdiv_ne_zero : 0 < pdivlcm_w
K5 : pdivlcm_w = 2
⊢ False
Tactic:
have := dvd_lcm_left l (p : ℕ)
State after:
case intro.inr
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 = 2 * ↑p
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
pdiv_ne_zero : 0 < pdivlcm_w
K5 : pdivlcm_w = 2
this : l ∣ lcm l ↑p
⊢ False

State before:
case intro.inr
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 = 2 * ↑p
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
pdiv_ne_zero : 0 < pdivlcm_w
K5 : pdivlcm_w = 2
this : l ∣ lcm l ↑p
⊢ False
Tactic:
simp_rw [pdivlcm_h] at this
State after:
case intro.inr
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 = 2 * ↑p
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
pdiv_ne_zero : 0 < pdivlcm_w
K5 : pdivlcm_w = 2
this : l ∣ 2 * ↑p
⊢ False

State before:
case intro.inr
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 = 2 * ↑p
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
pdiv_ne_zero : 0 < pdivlcm_w
K5 : pdivlcm_w = 2
this : l ∣ 2 * ↑p
⊢ False
Tactic:
apply absurd this h
State after:
no goals

State before:
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
⊢ IsPrimitiveRoot ⟨x, hx⟩ l
Tactic:
have nezero : NeZero (l : 𝓞 K) := by
  refine' ⟨fun hzero => _⟩
  simp only [Nat.cast_eq_zero] at hzero
  simp [hzero] at hl
State after:
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
nezero : NeZero ↑l
⊢ IsPrimitiveRoot ⟨x, hx⟩ l

State before:
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
nezero : NeZero ↑l
⊢ IsPrimitiveRoot ⟨x, hx⟩ l
Tactic:
rw [isRoot_cyclotomic_iff.symm]
State after:
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
nezero : NeZero ↑l
⊢ (cyclotomic l ↥(integralClosure ℤ K)).IsRoot ⟨x, hx⟩

State before:
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
nezero : NeZero ↑l
⊢ (cyclotomic l ↥(integralClosure ℤ K)).IsRoot ⟨x, hx⟩
Tactic:
apply hhl
State after:
no goals

State before:
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
⊢ NeZero ↑l
Tactic:
refine' ⟨fun hzero => _⟩
State after:
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
hzero : ↑l = 0
⊢ False

State before:
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
hzero : ↑l = 0
⊢ False
Tactic:
simp only [Nat.cast_eq_zero] at hzero
State after:
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
hzero : l = 0
⊢ False

State before:
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
hzero : l = 0
⊢ False
Tactic:
simp [hzero] at hl
State after:
no goals

State before:
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
⊢ IsPrimitiveRoot x l
Tactic:
have : (algebraMap R K) ⟨x, hx⟩ = x := by rfl
State after:
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
this : (algebraMap (𝓞 K) K) ⟨x, hx⟩ = x
⊢ IsPrimitiveRoot x l

State before:
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
this : (algebraMap (𝓞 K) K) ⟨x, hx⟩ = x
⊢ IsPrimitiveRoot x l
Tactic:
have h4 := IsPrimitiveRoot.map_of_injective hpl' (f := algebraMap (𝓞 K) K)
State after:
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
this : (algebraMap (𝓞 K) K) ⟨x, hx⟩ = x
h4 : Function.Injective ⇑(algebraMap (𝓞 K) K) → IsPrimitiveRoot ((algebraMap (𝓞 K) K) ⟨x, hx⟩) l
⊢ IsPrimitiveRoot x l

State before:
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
this : (algebraMap (𝓞 K) K) ⟨x, hx⟩ = x
h4 : Function.Injective ⇑(algebraMap (𝓞 K) K) → IsPrimitiveRoot ((algebraMap (𝓞 K) K) ⟨x, hx⟩) l
⊢ IsPrimitiveRoot x l
Tactic:
rw [← this]
State after:
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
this : (algebraMap (𝓞 K) K) ⟨x, hx⟩ = x
h4 : Function.Injective ⇑(algebraMap (𝓞 K) K) → IsPrimitiveRoot ((algebraMap (𝓞 K) K) ⟨x, hx⟩) l
⊢ IsPrimitiveRoot ((algebraMap (𝓞 K) K) ⟨x, hx⟩) l

State before:
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
this : (algebraMap (𝓞 K) K) ⟨x, hx⟩ = x
h4 : Function.Injective ⇑(algebraMap (𝓞 K) K) → IsPrimitiveRoot ((algebraMap (𝓞 K) K) ⟨x, hx⟩) l
⊢ IsPrimitiveRoot ((algebraMap (𝓞 K) K) ⟨x, hx⟩) l
Tactic:
apply h4
State after:
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
this : (algebraMap (𝓞 K) K) ⟨x, hx⟩ = x
h4 : Function.Injective ⇑(algebraMap (𝓞 K) K) → IsPrimitiveRoot ((algebraMap (𝓞 K) K) ⟨x, hx⟩) l
⊢ Function.Injective ⇑(algebraMap (𝓞 K) K)

State before:
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
this : (algebraMap (𝓞 K) K) ⟨x, hx⟩ = x
h4 : Function.Injective ⇑(algebraMap (𝓞 K) K) → IsPrimitiveRoot ((algebraMap (𝓞 K) K) ⟨x, hx⟩) l
⊢ Function.Injective ⇑(algebraMap (𝓞 K) K)
Tactic:
apply IsFractionRing.injective
State after:
no goals

State before:
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
⊢ (algebraMap (𝓞 K) K) ⟨x, hx⟩ = x
Tactic:
rfl
State after:
no goals

State before:
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 * pdivlcm_w
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
⊢ 0 < pdivlcm_w
Tactic:
by_contra h
State after:
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 * pdivlcm_w
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
h : ¬0 < pdivlcm_w
⊢ False

State before:
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 * pdivlcm_w
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
h : ¬0 < pdivlcm_w
⊢ False
Tactic:
simp only [not_lt, le_zero_iff] at h
State after:
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 * pdivlcm_w
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
h : pdivlcm_w = 0
⊢ False

State before:
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 * pdivlcm_w
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
h : pdivlcm_w = 0
⊢ False
Tactic:
rw [h] at pdivlcm_h
State after:
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

State before:
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
Tactic:
simp only [MulZeroClass.mul_zero, lcm_eq_zero_iff, PNat.ne_zero, or_false_iff] at pdivlcm_h
State after:
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

State before:
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
Tactic:
apply absurd pdivlcm_h (ne_of_gt (Nat.pos_of_mem_divisors hl))
State after:
no goals