awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
hnegζ : IsPrimitiveRoot (-ζ) (2 * n)
k : ℕ
hkpos : 0 < k
hkn : x ^ k = 1
l : ℕ
hl : l ∈ k.divisors
hlroot : IsRoot (cyclotomic l K) x
h : l = 0
⊢ False

Tactic:
simp [h] at hl
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
hnegζ : IsPrimitiveRoot (-ζ) (2 * n)
k : ℕ
hkpos : 0 < k
hkn : x ^ k = 1
l : ℕ
hl : l ∈ k.divisors
hlroot : IsRoot (cyclotomic l K) x
⊢ NeZero l

Tactic:
have hlzero : NeZero l := ⟨fun h ↦ by simp [h] at hl⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
hnegζ : IsPrimitiveRoot (-ζ) (2 * n)
k : ℕ
hkpos : 0 < k
hkn : x ^ k = 1
l : ℕ
hl : l ∈ k.divisors
hlroot : IsRoot (cyclotomic l K) x
hlzero : NeZero l
⊢ NeZero.{u} (R := K) (↑l : K)

Tactic:
have : NeZero (l : K) := ⟨NeZero.natCast_ne l K⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
hnegζ : IsPrimitiveRoot (-ζ) (2 * n)
k : ℕ
hkpos : 0 < k
hkn : x ^ k = 1
l : ℕ
hl : l ∈ k.divisors
hlroot : IsRoot (cyclotomic l K) x
hlzero : NeZero l
this : NeZero.{u} (R := K) (↑l : K)
⊢ IsPrimitiveRoot x l

Tactic:
rw [isRoot_cyclotomic_iff] at hlroot

Premises used: Polynomial.isRoot_cyclotomic_iff
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
hnegζ : IsPrimitiveRoot (-ζ) (2 * n)
k : ℕ
hkpos : 0 < k
hkn : x ^ k = 1
l : ℕ
hl : l ∈ k.divisors
hlroot : IsRoot (cyclotomic l K) x
hlzero : NeZero l
this : NeZero.{u} (R := K) (↑l : K)
hlroot₁ : IsPrimitiveRoot x l
⊢ NeZero l

Tactic:
rw [isRoot_cyclotomic_iff] at hlroot

Premises used: Polynomial.isRoot_cyclotomic_iff
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
hnegζ : IsPrimitiveRoot (-ζ) (2 * n)
k : ℕ
hkpos : 0 < k
hkn : x ^ k = 1
l : ℕ
hl : l ∈ k.divisors
hlroot : IsRoot (cyclotomic l K) x
hlzero : NeZero l
this : NeZero.{u} (R := K) (↑l : K)
hlroot₁ : IsPrimitiveRoot x l
hlzero₁ : NeZero l
⊢ NeZero.{u} (R := K) (↑l : K)

Tactic:
rw [isRoot_cyclotomic_iff] at hlroot

Premises used: Polynomial.isRoot_cyclotomic_iff
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
hnegζ : IsPrimitiveRoot (-ζ) (2 * n)
k : ℕ
hkpos : 0 < k
hkn : x ^ k = 1
l : ℕ
hl : l ∈ k.divisors
hlroot : IsPrimitiveRoot x l
hlzero : NeZero l
this : NeZero.{u} (R := K) (↑l : K)
obtain : ∀ (a : ℕ) (ha : 2 * n = l * a), ∃ (r : ℕ), x = (-ζ) ^ r
⊢ ∃ (r : ℕ), x = (-ζ) ^ r

Tactic:
obtain ⟨a, ha⟩ := hlroot.dvd_of_isCyclotomicExtension n hlzero.1

Premises used: IsPrimitiveRoot.dvd_of_isCyclotomicExtension, NeZero.out
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
hnegζ : IsPrimitiveRoot (-ζ) (2 * n)
k : ℕ
hkpos : 0 < k
hkn : x ^ k = 1
l : ℕ
hl : l ∈ k.divisors
hlroot : IsPrimitiveRoot x l
hlzero : NeZero l
this : NeZero.{u} (R := K) (↑l : K)
a : ℕ
ha : 2 * n = l * a
rw : x ^ (l * a) = 1
rw₁ : (x ^ l) ^ a = 1
rw₂ : HPow.hPow (α := K) 1 a = 1
rw₃ rw₄ : Eq.{u + 1} (α := K) 1 1
⊢ x ^ (2 * n) = 1

Tactic:
rw [ha, pow_mul, hlroot.pow_eq_one, one_pow]

Premises used: one_pow, pow_mul, IsPrimitiveRoot.pow_eq_one
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
hnegζ : IsPrimitiveRoot (-ζ) (2 * n)
k : ℕ
hkpos : 0 < k
hkn : x ^ k = 1
l : ℕ
hl : l ∈ k.divisors
hlroot : IsPrimitiveRoot x l
hlzero : NeZero l
this : NeZero.{u} (R := K) (↑l : K)
a : ℕ
ha : 2 * n = l * a
⊢ x ^ (2 * n) = 1

Tactic:
replace hlroot : x ^ (2 * n) = 1 := by rw [ha, pow_mul, hlroot.pow_eq_one, one_pow]
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
hnegζ : IsPrimitiveRoot (-ζ) (2 * n)
k : ℕ
hkpos : 0 < k
hkn : x ^ k = 1
l : ℕ
hl : l ∈ k.divisors
hlzero : NeZero l
this : NeZero.{u} (R := K) (↑l : K)
a : ℕ
ha : 2 * n = l * a
hlroot : x ^ (2 * n) = 1
obtain : ∀ (s : ℕ) (hs : (-ζ) ^ s = x), ∃ (r : ℕ), x = (-ζ) ^ r
⊢ ∃ (r : ℕ), x = (-ζ) ^ r

Tactic:
obtain ⟨s, -, hs⟩ := hnegζ.eq_pow_of_pow_eq_one hlroot

Premises used: IsPrimitiveRoot.eq_pow_of_pow_eq_one
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
hnegζ : IsPrimitiveRoot (-ζ) (2 * n)
k : ℕ
hkpos : 0 < k
hkn : x ^ k = 1
l : ℕ
hl : l ∈ k.divisors
hlzero : NeZero l
this : NeZero.{u} (R := K) (↑l : K)
a : ℕ
ha : 2 * n = l * a
hlroot : x ^ (2 * n) = 1
s : ℕ
hs : (-ζ) ^ s = x
⊢ ∃ (r : ℕ), x = (-ζ) ^ r

Tactic:
⟨s, hs.symm⟩

Premises used: Exists.intro, Eq.symm
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
hnegζ : IsPrimitiveRoot (-ζ) (2 * n)
k : ℕ
hkpos : 0 < k
hkn : x ^ k = 1
l : ℕ
hl : l ∈ k.divisors
hlzero : NeZero l
this : NeZero.{u} (R := K) (↑l : K)
a : ℕ
ha : 2 * n = l * a
hlroot : x ^ (2 * n) = 1
s : ℕ
hs : (-ζ) ^ s = x
⊢ ∃ (r : ℕ), x = (-ζ) ^ r

Tactic:
exact ⟨s, hs.symm⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
obtain : ∀ (r : ℕ) (hr : x = (-ζ) ^ r), ∃ r < n, x = ζ ^ r ∨ x = -ζ ^ r
⊢ ∃ r < n, x = ζ ^ r ∨ x = -ζ ^ r

Tactic:
obtain ⟨r, hr⟩ := hζ.exists_neg_pow_of_isOfFinOrder hno hx

Premises used: IsPrimitiveRoot.exists_neg_pow_of_isOfFinOrder
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
r : ℕ
hr : x = (-ζ) ^ r
⊢ ∃ r < n, x = ζ ^ r ∨ x = -ζ ^ r

Tactic:
⟨r % n, Nat.mod_lt _ (NeZero.pos _), ?_⟩

Premises used: Nat.mod_lt, HMod.hMod, And.intro, Exists.intro, NeZero.pos
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
r : ℕ
hr : x = (-ζ) ^ r
refine : x = ζ ^ (r % n) ∨ x = -ζ ^ (r % n)
⊢ ∃ r < n, x = ζ ^ r ∨ x = -ζ ^ r

Tactic:
refine ⟨r % n, Nat.mod_lt _ (NeZero.pos _), ?_⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
r : ℕ
hr : x = (-ζ) ^ r
rw : (-ζ) ^ r = ζ ^ r ∨ (-ζ) ^ r = -ζ ^ r
⊢ x = ζ ^ (r % n) ∨ x = -ζ ^ (r % n)

Tactic:
rw [show ζ ^ (r % n) = ζ ^ r from (IsPrimitiveRoot.eq_orderOf hζ).symm ▸ pow_mod_orderOf .., hr]

Premises used: IsPrimitiveRoot.eq_orderOf, pow_mod_orderOf, Eq.rec, Eq.symm
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
r : ℕ
hr : x = (-ζ) ^ r
inl : ∀ (h : Even r), (-ζ) ^ r = ζ ^ r ∨ (-ζ) ^ r = -ζ ^ r
inr : ∀ (h : Odd r), (-ζ) ^ r = ζ ^ r ∨ (-ζ) ^ r = -ζ ^ r
⊢ (-ζ) ^ r = ζ ^ r ∨ (-ζ) ^ r = -ζ ^ r

Tactic:
rcases Nat.even_or_odd r with (h | h)

Premises used: Nat.even_or_odd
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
r : ℕ
hr : x = (-ζ) ^ r
h : Even r
⊢ (-ζ) ^ r = ζ ^ r ∨ (-ζ) ^ r = -ζ ^ r

Tactic:
simp [neg_pow, h.neg_one_pow]

Premises used: Even.neg_one_pow, neg_pow
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
r : ℕ
hr : x = (-ζ) ^ r
h : Odd r
⊢ (-ζ) ^ r = ζ ^ r ∨ (-ζ) ^ r = -ζ ^ r

Tactic:
simp [neg_pow, h.neg_one_pow]

Premises used: neg_pow, Odd.neg_one_pow
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
K : Type u
L : Type v
inst : CommRing L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
hζ : IsPrimitiveRoot ζ 2
inst_3 : IsDomain L
⊢ Eq.{v + 1} (α := L) (-1 : L) ((algebraMap K L : (a : K) → L) (-1) : L)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
K : Type u
L : Type v
inst : CommRing L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
hζ : IsPrimitiveRoot ζ 2
inst_3 : IsDomain L
rw : (Algebra.norm K : (a : L) → K) (-1) = HPow.hPow (α := K) (-1) (Module.finrank K L)
rw₁ :
  (Algebra.norm K : (a : L) → K) ((algebraMap K L : (a : K) → L) (-1) : L) =
    HPow.hPow (α := K) (-1) (Module.finrank K L)
rw₂ rw₃ : HPow.hPow (α := K) (-1) (Module.finrank K L) = HPow.hPow (α := K) (-1) (Module.finrank K L)
⊢ (Algebra.norm K : (a : L) → K) ζ = HPow.hPow (α := K) (-1) (Module.finrank K L)

Tactic:
rw [hζ.eq_neg_one_of_two_right, show -1 = algebraMap K L (-1) by simp, Algebra.norm_algebraMap]

Premises used: Algebra.norm_algebraMap, IsPrimitiveRoot.eq_neg_one_of_two_right
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : CommRing L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_4 : IsDomain L
inst_5 : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (M := K[X]) (cyclotomic n K)
⊢ NeZero.{u} (R := K) (↑n : K)

Tactic:
haveI := IsCyclotomicExtension.neZero' n K L
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : CommRing L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_4 : IsDomain L
inst_5 : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this : NeZero.{u} (R := K) (↑n : K)
pos : ∀ (h1 : n = 1), Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) ζ : K) (1 : K)
neg : ∀ (h1 : ¬n = 1), Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) ζ : K) (1 : K)
⊢ Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) ζ : K) (1 : K)

Tactic:
by_cases h1 : n = 1
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : CommRing L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_4 : IsDomain L
inst_5 : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this : NeZero.{u} (R := K) (↑n : K)
h1 : n = 1
⊢ ζ = 1

Tactic:
rw [h1, one_right_iff] at hζ

Premises used: IsPrimitiveRoot.one_right_iff
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : CommRing L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_4 : IsDomain L
inst_5 : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this : NeZero.{u} (R := K) (↑n : K)
h1 : n = 1
hζ₁ : ζ = 1
⊢ IsDomain L

Tactic:
rw [h1, one_right_iff] at hζ

Premises used: IsPrimitiveRoot.one_right_iff
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst_1 : NeZero n
K : Type u
L : Type v
inst_2 : CommRing L
ζ : L
inst_3 : Field K
inst_4 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_5 : IsDomain L
inst_6 : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this : NeZero.{u} (R := K) (↑n : K)
h1 : n = 1
hζ₁ : ζ = 1
inst : IsDomain L
⊢ IsCyclotomicExtension {n} K L

Tactic:
rw [h1, one_right_iff] at hζ

Premises used: IsPrimitiveRoot.one_right_iff
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst_1 : NeZero n
K : Type u
L : Type v
inst_2 : CommRing L
ζ : L
inst_3 : Field K
inst_4 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_5 : IsDomain L
inst_6 : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this : NeZero.{u} (R := K) (↑n : K)
h1 : n = 1
hζ₁ : ζ = 1
inst : IsDomain L
inst₁ : IsCyclotomicExtension {n} K L
⊢ n ≠ 2

Tactic:
rw [h1, one_right_iff] at hζ

Premises used: IsPrimitiveRoot.one_right_iff
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst_1 : NeZero n
K : Type u
L : Type v
inst_2 : CommRing L
ζ : L
inst_3 : Field K
inst_4 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_5 : IsDomain L
inst_6 : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this : NeZero.{u} (R := K) (↑n : K)
h1 : n = 1
hζ₁ : ζ = 1
inst : IsDomain L
inst₁ : IsCyclotomicExtension {n} K L
hn₁ : n ≠ 2
⊢ Irreducible (M := K[X]) (cyclotomic n K)

Tactic:
rw [h1, one_right_iff] at hζ

Premises used: IsPrimitiveRoot.one_right_iff
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst_1 : NeZero n
K : Type u
L : Type v
inst_2 : CommRing L
ζ : L
inst_3 : Field K
inst_4 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_5 : IsDomain L
inst_6 : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this : NeZero.{u} (R := K) (↑n : K)
h1 : n = 1
hζ₁ : ζ = 1
inst : IsDomain L
inst₁ : IsCyclotomicExtension {n} K L
hn₁ : n ≠ 2
hirr₁ : Irreducible (M := K[X]) (cyclotomic n K)
⊢ NeZero.{u} (R := K) (↑n : K)

Tactic:
rw [h1, one_right_iff] at hζ

Premises used: IsPrimitiveRoot.one_right_iff
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst_1 : NeZero n
K : Type u
L : Type v
inst_2 : CommRing L
ζ : L
inst_3 : Field K
inst_4 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_5 : IsDomain L
inst_6 : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this : NeZero.{u} (R := K) (↑n : K)
h1 : n = 1
hζ₁ : ζ = 1
inst : IsDomain L
inst₁ : IsCyclotomicExtension {n} K L
hn₁ : n ≠ 2
hirr₁ : Irreducible (M := K[X]) (cyclotomic n K)
this₁ : NeZero.{u} (R := K) (↑n : K)
⊢ n = 1

Tactic:
rw [h1, one_right_iff] at hζ

Premises used: IsPrimitiveRoot.one_right_iff
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : CommRing L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : ζ = 1
inst_4 : IsDomain L
inst_5 : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this : NeZero.{u} (R := K) (↑n : K)
h1 : n = 1
⊢ Eq.{v + 1} (α := L) (1 : L) ((algebraMap K L : (a : K) → L) 1 : L)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : CommRing L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : ζ = 1
inst_4 : IsDomain L
inst_5 : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this : NeZero.{u} (R := K) (↑n : K)
h1 : n = 1
pos : Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) 1 : K) (1 : K)
pos₁ : Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) ((algebraMap K L : (a : K) → L) 1 : L) : K) (1 : K)
pos₂ : HPow.hPow (α := K) 1 (Module.finrank K L) = 1
pos₃ pos₄ : Eq.{u + 1} (α := K) 1 1
⊢ Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) ζ : K) (1 : K)

Tactic:
rw [hζ, show 1 = algebraMap K L 1 by simp, Algebra.norm_algebraMap, one_pow]

Premises used: one_pow, Algebra.norm_algebraMap
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : CommRing L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_4 : IsDomain L
inst_5 : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this : NeZero.{u} (R := K) (↑n : K)
h1 : ¬n = 1
⊢ 2 ≤ n

Tactic:
replace h1 : 2 ≤ n := (two_le_iff n).mpr ⟨NeZero.ne _, h1⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : CommRing L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_4 : IsDomain L
inst_5 : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this : NeZero.{u} (R := K) (↑n : K)
h1 : 2 ≤ n
neg : HPow.hPow (α := K) (-1) (φ n) = 1
⊢ Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) ζ : K) (1 : K)

Tactic:
rw [← hζ.powerBasis_gen K, PowerBasis.norm_gen_eq_coeff_zero_minpoly, hζ.powerBasis_gen K,
      ← hζ.minpoly_eq_cyclotomic_of_irreducible hirr, cyclotomic_coeff_zero K h1, mul_one,
      hζ.powerBasis_dim K, ← hζ.minpoly_eq_cyclotomic_of_irreducible hirr, natDegree_cyclotomic]

Premises used: Algebra.PowerBasis.norm_gen_eq_coeff_zero_minpoly, IsPrimitiveRoot.powerBasis_dim, Polynomial.natDegree_cyclotomic, IsPrimitiveRoot.powerBasis_gen, Polynomial.cyclotomic_coeff_zero, IsPrimitiveRoot.minpoly_eq_cyclotomic_of_irreducible, mul_one
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : CommRing L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_4 : IsDomain L
inst_5 : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this : NeZero.{u} (R := K) (↑n : K)
h1 : 2 ≤ n
⊢ HPow.hPow (α := K) (-1) (φ n) = 1

Tactic:
(totient_even <| h1.lt_of_ne hn.symm).neg_one_pow

Premises used: Ne.symm, Even.neg_one_pow, LE.le.lt_of_ne, Nat.totient_even
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : CommRing L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_4 : IsDomain L
inst_5 : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this : NeZero.{u} (R := K) (↑n : K)
h1 : 2 ≤ n
⊢ HPow.hPow (α := K) (-1) (φ n) = 1

Tactic:
exact (totient_even <| h1.lt_of_ne hn.symm).neg_one_pow

Premises used: Ne.symm, Even.neg_one_pow, LE.le.lt_of_ne, Nat.totient_even
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
L : Type v
inst : CommRing L
ζ : L
hζ : IsPrimitiveRoot ζ n
K : Type u_1
inst_1 : Field K
inst_2 : LinearOrder K
inst_3 : IsStrictOrderedRing K
inst_4 : Algebra K L
hodd : Odd n
⊢ Eq.{u_1 + 1} (α := K) ((Algebra.norm K : (a : L) → K) (ζ ^ n) : K) ((Algebra.norm K : (a : L) → K) 1 : K)

Tactic:
have hz := congr_arg (norm K) ((IsPrimitiveRoot.iff_def _ n).1 hζ).1
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
L : Type v
inst : CommRing L
ζ : L
hζ : IsPrimitiveRoot ζ n
K : Type u_1
inst_1 : Field K
inst_2 : LinearOrder K
inst_3 : IsStrictOrderedRing K
inst_4 : Algebra K L
hodd : Odd n
hz : Eq.{u_1 + 1} (α := K) ((Algebra.norm K : (a : L) → K) (ζ ^ n) : K) ((Algebra.norm K : (a : L) → K) 1 : K)
⊢ HPow.hPow (α := K) ((Algebra.norm K : (a : L) → K) ζ : K) n = HPow.hPow (α := K) 1 n

Tactic:
rw [← (algebraMap K L).map_one, Algebra.norm_algebraMap, one_pow, map_pow, ← one_pow n] at hz

Premises used: one_pow, Algebra.algebraMap, RingHom.map_one, map_pow, Algebra.norm_algebraMap
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
L : Type v
inst : CommRing L
ζ : L
hζ : IsPrimitiveRoot ζ n
K : Type u_1
inst_1 : Field K
inst_2 : LinearOrder K
inst_3 : IsStrictOrderedRing K
inst_4 : Algebra K L
hodd : Odd n
hz : HPow.hPow (α := K) ((Algebra.norm K : (a : L) → K) ζ : K) n = HPow.hPow (α := K) 1 n
⊢ Eq.{u_1 + 1} (α := K) ((Algebra.norm K : (a : L) → K) ζ : K) (1 : K)

Tactic:
StrictMono.injective hodd.strictMono_pow hz

Premises used: Odd.strictMono_pow, StrictMono.injective
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
L : Type v
inst : CommRing L
ζ : L
hζ : IsPrimitiveRoot ζ n
K : Type u_1
inst_1 : Field K
inst_2 : LinearOrder K
inst_3 : IsStrictOrderedRing K
inst_4 : Algebra K L
hodd : Odd n
hz : HPow.hPow (α := K) ((Algebra.norm K : (a : L) → K) ζ : K) n = HPow.hPow (α := K) 1 n
⊢ Eq.{u_1 + 1} (α := K) ((Algebra.norm K : (a : L) → K) ζ : K) (1 : K)

Tactic:
exact StrictMono.injective hodd.strictMono_pow hz

Premises used: Odd.strictMono_pow, StrictMono.injective
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : CommRing L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_4 : IsDomain L
inst_5 : IsCyclotomicExtension {n} K L
hirr : Irreducible (M := K[X]) (cyclotomic n K)
pos : ∀ (hn : n = 2), Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) ζ : K) (-1 : K)
neg : ∀ (hn : ¬n = 2), Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) ζ : K) (1 : K)
⊢ Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) ζ : K) (if n = 2 then -1 else 1 : K)

Tactic:
split_ifs with hn
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : CommRing L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_4 : IsDomain L
inst_5 : IsCyclotomicExtension {n} K L
hirr : Irreducible (M := K[X]) (cyclotomic n K)
hn : n = 2
⊢ NeZero (R := ℕ) 2

Tactic:
subst hn
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst_1 : NeZero n
K : Type u
L : Type v
inst_2 : CommRing L
ζ : L
inst_3 : Field K
inst_4 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_5 : IsDomain L
inst_6 : IsCyclotomicExtension {n} K L
hirr : Irreducible (M := K[X]) (cyclotomic n K)
hn : n = 2
inst : NeZero (R := ℕ) 2
⊢ IsPrimitiveRoot ζ 2

Tactic:
subst hn
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst_1 : NeZero n
K : Type u
L : Type v
inst_2 : CommRing L
ζ : L
inst_3 : Field K
inst_4 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_5 : IsDomain L
inst_6 : IsCyclotomicExtension {n} K L
hirr : Irreducible (M := K[X]) (cyclotomic n K)
hn : n = 2
inst : NeZero (R := ℕ) 2
hζ₁ : IsPrimitiveRoot ζ 2
⊢ IsCyclotomicExtension {2} K L

Tactic:
subst hn
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst_1 : NeZero n
K : Type u
L : Type v
inst_2 : CommRing L
ζ : L
inst_3 : Field K
inst_4 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_5 : IsDomain L
inst_6 : IsCyclotomicExtension {n} K L
hirr : Irreducible (M := K[X]) (cyclotomic n K)
hn : n = 2
inst : NeZero (R := ℕ) 2
hζ₁ : IsPrimitiveRoot ζ 2
inst₁ : IsCyclotomicExtension {2} K L
⊢ Irreducible (M := K[X]) (cyclotomic 2 K)

Tactic:
subst hn
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
K : Type u
L : Type v
inst : CommRing L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
inst_3 : IsDomain L
inst_4 : NeZero (R := ℕ) 2
hζ : IsPrimitiveRoot ζ 2
inst_5 : IsCyclotomicExtension {2} K L
hirr : Irreducible (M := K[X]) (cyclotomic 2 K)
pos : HPow.hPow (α := K) (-1) (φ 2) = -1
⊢ Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) ζ : K) (-1 : K)

Tactic:
rw [norm_eq_neg_one_pow (K := K) hζ, IsCyclotomicExtension.finrank _ hirr]

Premises used: IsPrimitiveRoot.norm_eq_neg_one_pow, IsCyclotomicExtension.finrank