mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i, C (α i) * X ^ ↑i
hP : ∀ (i : Fin p), α i = P.coeff ↑i
x✝¹ : Fin p
x✝ : x✝¹ ∈ Finset.univ
⊢ ↑x✝¹ ≤ p - 1

Tactic:
;

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i, C (α i) * X ^ ↑i
hP : ∀ (i : Fin p), α i = P.coeff ↑i
x✝¹ : Fin p
x✝ : x✝¹ ∈ Finset.univ
⊢ ↑x✝¹ ≤ p - 1
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ⋯
hP : ∀ (i : Fin p), α i = P.coeff ↑i
hP' : P.degree ≤ ↑(p - 1)
⊢ ∑ i, ↑(α i) * ζ ^ ↑i = 0 ↔ (aeval ζ) P = 0

pp: K : Type u_1
inst✝¹ : Field K
inst✝ : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ⋯
hP : ∀ (i : Fin p), α i = P.coeff ↑i
hP' : P.degree ≤ ↑(p - 1)
⊢ (aeval ζ) P = 0 ↔ ∀ (i j : Fin p), α i = α j

Tactic:
;

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ⋯
hP : ∀ (i : Fin p), α i = P.coeff ↑i
hP' : P.degree ≤ ↑(p - 1)
⊢ ∑ i, ↑(α i) * ζ ^ ↑i = 0 ↔ (aeval ζ) P = 0

K : Type u_1
inst✝¹ : Field K
inst✝ : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ⋯
hP : ∀ (i : Fin p), α i = P.coeff ↑i
hP' : P.degree ≤ ↑(p - 1)
⊢ (aeval ζ) P = 0 ↔ ∀ (i j : Fin p), α i = α j
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i, C (α i) * X ^ ↑i
hP : ∀ (i : Fin p), α i = P.coeff ↑i
hP' : P.degree ≤ ↑(p - 1)
H : ∀ (i j : Fin p), α i = α j
i : Fin p
⊢ P.coeff ↑i = (cyclotomic p ℚ * C (α 0)).coeff ↑i

Tactic:
;

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i, C (α i) * X ^ ↑i
hP : ∀ (i : Fin p), α i = P.coeff ↑i
hP' : P.degree ≤ ↑(p - 1)
H : ∀ (i j : Fin p), α i = α j
i : Fin p
⊢ P.coeff ↑i = (cyclotomic p ℚ * C (α 0)).coeff ↑i
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
⊢ X ^ 3 + 1 = (X ^ 2 - X + 1) * (X + 1)

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : Ring R
⊢ X ^ 3 + 1 = (X ^ 2 - X + 1) * (X + 1)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Goal state before:
pp: R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ⋯
⊢ (fun x ↦ cyclotomic n (ZMod p) * x) (cyclotomic (n * p) (ZMod p)) =
    (fun x ↦ cyclotomic n (ZMod p) * x) (cyclotomic n (ZMod p) ^ (p - 1))

Tactic:
;

Goal state after:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ⋯
⊢ (fun x ↦ cyclotomic n (ZMod p) * x) (cyclotomic (n * p) (ZMod p)) =
    (fun x ↦ cyclotomic n (ZMod p) * x) (cyclotomic n (ZMod p) ^ (p - 1))
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: case succ.succ.succ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℕ
⊢ (1 < x → 0 < eval x (cyclotomic (n + 1 + 1 + 1) R)) ∧ (1 ≤ x → 0 ≤ eval x (cyclotomic (n + 1 + 1 + 1) R))

Tactic:
· constructor <;> intro <;> [skip; apply le_of_lt] <;> apply cyclotomic_pos (by lia)

Goal state after:
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: K : Type u_1
F : Type u_2
inst✝³ : Field K
inst✝² : Fintype K
inst✝¹ : Field F
inst✝ : Algebra F K
⊢ Algebra.adjoin F ↑univ.val.toFinset = ⊤

Tactic:
val_toFinset,

Goal state after:
K : Type u_1
F : Type u_2
inst✝³ : Field K
inst✝² : Fintype K
inst✝¹ : Field F
inst✝ : Algebra F K
⊢ Algebra.adjoin F ↑univ = ⊤
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: case zero
n : ℕ
h : n ≠ 0
h_prime : Fact (Nat.Prime 0)
this : Fintype (GaloisField 0 n)
g_poly : (ZMod 0)[X] := X ^ 0 ^ n - X
hp : 1 < 0
aux : g_poly ≠ 0
key : Fintype.card ↑(g_poly.rootSet (GaloisField 0 n)) = 0 ^ n
nat_degree_eq : g_poly.natDegree = 0 ^ n
x : GaloisField 0 n
hx :
  x ∈
    Subring.closure
      (Set.range ⇑(algebraMap (ZMod 0) (GaloisField 0 n)) ∪ (X ^ 0 ^ n - X).rootSet (X ^ 0 ^ n - X).SplittingField)
⊢ x ∈ (X ^ 0 ^ n - X).rootSet (GaloisField 0 n)

pp: case succ
n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (n✝ + 1))
this : Fintype (GaloisField (n✝ + 1) n)
g_poly : (ZMod (n✝ + 1))[X] := X ^ (n✝ + 1) ^ n - X
hp : 1 < n✝ + 1
aux : g_poly ≠ 0
key : Fintype.card ↑(g_poly.rootSet (GaloisField (n✝ + 1) n)) = (n✝ + 1) ^ n
nat_degree_eq : g_poly.natDegree = (n✝ + 1) ^ n
x : GaloisField (n✝ + 1) n
hx :
  x ∈
    Subring.closure
      (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
        (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField)
⊢ x ∈ (X ^ (n✝ + 1) ^ n - X).rootSet (GaloisField (n✝ + 1) n)

Tactic:
;

Goal state after:
case zero
n : ℕ
h : n ≠ 0
h_prime : Fact (Nat.Prime 0)
this : Fintype (GaloisField 0 n)
g_poly : (ZMod 0)[X] := X ^ 0 ^ n - X
hp : 1 < 0
aux : g_poly ≠ 0
key : Fintype.card ↑(g_poly.rootSet (GaloisField 0 n)) = 0 ^ n
nat_degree_eq : g_poly.natDegree = 0 ^ n
x : GaloisField 0 n
hx :
  x ∈
    Subring.closure
      (Set.range ⇑(algebraMap (ZMod 0) (GaloisField 0 n)) ∪ (X ^ 0 ^ n - X).rootSet (X ^ 0 ^ n - X).SplittingField)
⊢ x ∈ (X ^ 0 ^ n - X).rootSet (GaloisField 0 n)

case succ
n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (n✝ + 1))
this : Fintype (GaloisField (n✝ + 1) n)
g_poly : (ZMod (n✝ + 1))[X] := X ^ (n✝ + 1) ^ n - X
hp : 1 < n✝ + 1
aux : g_poly ≠ 0
key : Fintype.card ↑(g_poly.rootSet (GaloisField (n✝ + 1) n)) = (n✝ + 1) ^ n
nat_degree_eq : g_poly.natDegree = (n✝ + 1) ^ n
x : GaloisField (n✝ + 1) n
hx :
  x ∈
    Subring.closure
      (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
        (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField)
⊢ x ∈ (X ^ (n✝ + 1) ^ n - X).rootSet (GaloisField (n✝ + 1) n)
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_1.inl
S T : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
x : B
n : ℕ
hnpow : n ≠ 0 ∧ x ^ n = 1
hn₁ : n ∈ S
⊢ x ∈ {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}

Tactic:
;

Goal state after:
case refine_1.inl
S T : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
x : B
n : ℕ
hnpow : n ≠ 0 ∧ x ^ n = 1
hn₁ : n ∈ S
⊢ x ∈ {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_1.inr
S T : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
x : B
n : ℕ
hnpow : n ≠ 0 ∧ x ^ n = 1
hn₂ : n ∈ T
⊢ x ∈ {b | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1}

Tactic:
;

Goal state after:
case refine_1.inr
S T : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
x : B
n : ℕ
hnpow : n ≠ 0 ∧ x ^ n = 1
hn₂ : n ∈ T
⊢ x ∈ {b | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1}
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: case convert_2
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := ⋯
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖↑q - ζ'‖
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ ↥(primitiveRoots n ℂ) → NNRealˣ

pp: case e'_3
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖↑q - ζ'‖
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ Units.mk0 (q - 1).toNNReal ⋯ ^ φ n = ∏ i ∈ (primitiveRoots n ℂ).attach, ?convert_2 i

pp: case convert_5
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖↑q - ζ'‖
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ ∀ i ∈ (primitiveRoots n ℂ).attach, ?convert_2 i ≤ Units.mk0 ‖↑q - ↑i‖₊ ⋯

pp: case convert_6
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖↑q - ζ'‖
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ ∃ i ∈ (primitiveRoots n ℂ).attach, ?convert_2 i < Units.mk0 ‖↑q - ↑i‖₊ ⋯

Tactic:
;

Goal state after:
case convert_2
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := ⋯
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖↑q - ζ'‖
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ ↥(primitiveRoots n ℂ) → NNRealˣ

case e'_3
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖↑q - ζ'‖
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ Units.mk0 (q - 1).toNNReal ⋯ ^ φ n = ∏ i ∈ (primitiveRoots n ℂ).attach, ?convert_2 i

case convert_5
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖↑q - ζ'‖
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ ∀ i ∈ (primitiveRoots n ℂ).attach, ?convert_2 i ≤ Units.mk0 ‖↑q - ↑i‖₊ ⋯

case convert_6
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖↑q - ζ'‖
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ ∃ i ∈ (primitiveRoots n ℂ).attach, ?convert_2 i < Units.mk0 ‖↑q - ↑i‖₊ ⋯
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: n : ℕ
inst✝⁴ : NeZero n
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst✝ : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (cyclotomic n K)
this✝² : NeZero ↑n
E : Type v := AlgebraicClosure L
z : E
hz : (cyclotomic n E).IsRoot z
this✝¹ : FiniteDimensional K L := finiteDimensional {n} K L
this✝ : IsGalois K L := isGalois {n} K L
Hprod : ∏ σ, (1 - σ ζ) = eval 1 (cyclotomic' n E)
this : NeZero ↑n
⊢ ∏ x, (1 - x ζ) = (algebraMap K E) ↑(eval 1 (cyclotomic n ℤ))

Tactic:
rw [Hprod, cyclotomic', ← cyclotomic_eq_prod_X_sub_primitiveRoots (isRoot_cyclotomic_iff.1 hz),
    ← map_cyclotomic_int, _root_.map_intCast, ← Int.cast_one, eval_intCast_map, eq_intCast,
    Int.cast_id]

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case neg
S : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
hS : ¬∃ s ∈ S, s ≠ 0
⊢ IsCyclotomicExtension S A B ↔ IsCyclotomicExtension (S ∪ {1}) A B

Tactic:
rw [eq_self_sdiff_zero S, eq_self_sdiff_zero (S ∪ {1}), union_sdiff_distrib,
      show S \ {0} = ∅ by aesop, empty_union, show {1} \ {0} = {1} by simp]

Goal state after:
case neg
S : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
hS : ¬∃ s ∈ S, s ≠ 0
⊢ IsCyclotomicExtension ∅ A B ↔ IsCyclotomicExtension {1} A B
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ < q + 1
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ 0 < q + 1

Tactic:
;

Goal state after:
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ < q + 1
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ 0 < q + 1
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case empty
S : Set ℕ
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h₂ : IsCyclotomicExtension ∅ A B
⊢ Submodule.span A ↑{1} = ⊤

Tactic:
simp [← top_toSubmodule, ← subsingleton_iff_bot_eq_top.mpr inferInstance,
      toSubmodule_bot, Submodule.one_eq_span]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ < q + 1
this✝ : ¬eval (↑q) (cyclotomic n ℂ) = 0
this : Units.mk0 ‖eval (↑q) (cyclotomic n ℂ)‖₊ ⋯ < Units.mk0 (q + 1).toNNReal ⋯ ^ φ n
⊢ eval q (cyclotomic n ℝ) < (q + 1) ^ φ n

Tactic:
by
    simp only [← Units.val_lt_val, Units.val_pow_eq_pow_val, Units.val_mk0, ← NNReal.coe_lt_coe,
      coe_nnnorm, NNReal.coe_pow,
      Real.coe_toNNReal'] at this
    convert! this using 2
    · rw [eq_comm]
      simp [cyclotomic_nonneg n hq'.le]
    rw [eq_comm, max_eq_left_iff]
    linarith

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: case convert_3
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := ⋯
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ < q + 1
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ ↥(primitiveRoots n ℂ) → NNRealˣ

pp: case e'_4
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ < q + 1
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ Units.mk0 (q + 1).toNNReal ⋯ ^ φ n = ∏ i ∈ (primitiveRoots n ℂ).attach, ?convert_3 i

pp: case convert_5
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ < q + 1
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ ∀ i ∈ (primitiveRoots n ℂ).attach, Units.mk0 ‖↑q - ↑i‖₊ ⋯ ≤ ?convert_3 i

pp: case convert_6
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ < q + 1
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ ∃ i ∈ (primitiveRoots n ℂ).attach, Units.mk0 ‖↑q - ↑i‖₊ ⋯ < ?convert_3 i

Tactic:
;

Goal state after:
case convert_3
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := ⋯
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ < q + 1
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ ↥(primitiveRoots n ℂ) → NNRealˣ

case e'_4
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ < q + 1
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ Units.mk0 (q + 1).toNNReal ⋯ ^ φ n = ∏ i ∈ (primitiveRoots n ℂ).attach, ?convert_3 i

case convert_5
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ < q + 1
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ ∀ i ∈ (primitiveRoots n ℂ).attach, Units.mk0 ‖↑q - ↑i‖₊ ⋯ ≤ ?convert_3 i

case convert_6
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ < q + 1
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ ∃ i ∈ (primitiveRoots n ℂ).attach, Units.mk0 ‖↑q - ↑i‖₊ ⋯ < ?convert_3 i
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: case refine_1
p : ℕ
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
this✝¹ : IsCyclotomicExtension {p ^ (k - s + 1)} K ↥K⟮η⟯
hη : IsPrimitiveRoot (η₁ + 1) (p ^ (k - s + 1))
this✝ : FiniteDimensional K L
this : IsGalois K L
⊢ IsPrimePow (p ^ (k - s + 1))

pp: case refine_2
p : ℕ
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
this✝¹ : IsCyclotomicExtension {p ^ (k - s + 1)} K ↥K⟮η⟯
hη : IsPrimitiveRoot (η₁ + 1) (p ^ (k - s + 1))
this✝ : FiniteDimensional K L
this : IsGalois K L
H : (Algebra.norm K) (η₁ + 1 - 1) = ↑(p ^ (k - s + 1)).minFac
⊢ (Algebra.norm K) (IntermediateField.AdjoinSimple.gen K η) ^ Module.finrank (↥K⟮η⟯) L = ↑p ^ p ^ s

Tactic:
;

Goal state after:
case refine_1
p : ℕ
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
this✝¹ : IsCyclotomicExtension {p ^ (k - s + 1)} K ↥K⟮η⟯
hη : IsPrimitiveRoot (η₁ + 1) (p ^ (k - s + 1))
this✝ : FiniteDimensional K L
this : IsGalois K L
⊢ IsPrimePow (p ^ (k - s + 1))

case refine_2
p : ℕ
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
this✝¹ : IsCyclotomicExtension {p ^ (k - s + 1)} K ↥K⟮η⟯
hη : IsPrimitiveRoot (η₁ + 1) (p ^ (k - s + 1))
this✝ : FiniteDimensional K L
this : IsGalois K L
H : (Algebra.norm K) (η₁ + 1 - 1) = ↑(p ^ (k - s + 1)).minFac
⊢ (Algebra.norm K) (IntermediateField.AdjoinSimple.gen K η) ^ Module.finrank (↥K⟮η⟯) L = ↑p ^ p ^ s
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: S : Set ℕ
K : Type w
L : Type z
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension S K L
M : Type u_1
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsSepClosed M
this : Algebra.IsSeparable K L
i : L →ₐ[K] M := IsSepClosed.lift
htop : IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1} = ⊤
⊢ IntermediateField.map i (IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) =
    IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}

Tactic:
IntermediateField.adjoin_map

Goal state after:
S : Set ℕ
K : Type w
L : Type z
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension S K L
M : Type u_1
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsSepClosed M
this : Algebra.IsSeparable K L
i : L →ₐ[K] M := IsSepClosed.lift
htop : IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1} = ⊤
⊢ IntermediateField.adjoin K (⇑i '' {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) =
    IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: case neg
n : ℕ
x : ℤ
h : x.gcd ↑n = 1
hn : ¬n = 0
this : NeZero n
⊢ (↑x).val.Coprime n

Tactic:
← Int.gcd_emod,

Goal state after:
case neg
n : ℕ
x : ℤ
h : (x % ↑n).gcd ↑n = 1
hn : ¬n = 0
this : NeZero n
⊢ (↑x).val.Coprime n
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: case zero
h_prime : Fact (Nat.Prime 0)
hp : 1 < 0
h1 : (X ^ 0 - X).roots = univ.val
h2 : (X ^ 0 - X).natDegree = 0
⊢ (X ^ 0 - X).Splits

pp: case succ
n✝ : ℕ
h_prime : Fact (Nat.Prime (n✝ + 1))
hp : 1 < n✝ + 1
h1 : (X ^ (n✝ + 1) - X).roots = univ.val
h2 : (X ^ (n✝ + 1) - X).natDegree = n✝ + 1
⊢ (X ^ (n✝ + 1) - X).Splits

Tactic:
;

Goal state after:
case zero
h_prime : Fact (Nat.Prime 0)
hp : 1 < 0
h1 : (X ^ 0 - X).roots = univ.val
h2 : (X ^ 0 - X).natDegree = 0
⊢ (X ^ 0 - X).Splits

case succ
n✝ : ℕ
h_prime : Fact (Nat.Prime (n✝ + 1))
hp : 1 < n✝ + 1
h1 : (X ^ (n✝ + 1) - X).roots = univ.val
h2 : (X ^ (n✝ + 1) - X).natDegree = n✝ + 1
⊢ (X ^ (n✝ + 1) - X).Splits
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: p✝ : ℕ
inst✝ : Fact (Nat.Prime p✝)
n✝ p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : X ^ p ^ 1 = X ^ Fintype.card (ZMod p)
⊢ IsSplittingField (ZMod p) (ZMod p) (X ^ Fintype.card (ZMod p) - X)

Tactic:
;

Goal state after:
p✝ : ℕ
inst✝ : Fact (Nat.Prime p✝)
n✝ p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : X ^ p ^ 1 = X ^ Fintype.card (ZMod p)
⊢ IsSplittingField (ZMod p) (ZMod p) (X ^ Fintype.card (ZMod p) - X)
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ψ : AddChar (ZMod n) C
h₁ : ψ 1 = 1
a : ZMod n
⊢ a = ↑a.val

Tactic:
;

Goal state after:
C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ψ : AddChar (ZMod n) C
h₁ : ψ 1 = 1
a : ZMod n
⊢ a = ↑a.val
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: C : Type v
inst✝ : CommMonoid C
n : ℕ
ψ : AddChar (ZMod n) C
hψ : ∀ (a : ZMod n), ψ a = 1 → a = 0
a : ZMod n
ha : a ≠ 0
hf : ψ.mulShift a = 1
h : ψ a = 1 1
⊢ False

Tactic:
;

Goal state after:
C : Type v
inst✝ : CommMonoid C
n : ℕ
ψ : AddChar (ZMod n) C
hψ : ∀ (a : ZMod n), ψ a = 1 → a = 0
a : ZMod n
ha : a ≠ 0
hf : ψ.mulShift a = 1
h : ψ a = 1 1
⊢ False
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: K : Type u_1
K' : Type u_2
inst✝³ : Field K
inst✝² : Field K'
inst✝¹ : Algebra K K'
inst✝ : Finite K'
this✝ : Finite K
this : Fintype K'ˣ
⊢ (↑(Units.map (Algebra.norm K)).ker).ncard = (↑{a | a ^ ((Nat.card K' - 1) / (Nat.card K - 1)) = 1}).ncard

Tactic:
;

Goal state after:
K : Type u_1
K' : Type u_2
inst✝³ : Field K
inst✝² : Field K'
inst✝¹ : Algebra K K'
inst✝ : Finite K'
this✝ : Finite K
this : Fintype K'ˣ
⊢ (↑(Units.map (Algebra.norm K)).ker).ncard = (↑{a | a ^ ((Nat.card K' - 1) / (Nat.card K - 1)) = 1}).ncard
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: K : Type u_1
K' : Type u_2
inst✝³ : Field K
inst✝² : Field K'
inst✝¹ : Algebra K K'
inst✝ : Finite K'
this✝ : Finite K
this : Fintype K'ˣ
⊢ ↑(Units.map (Algebra.norm K)).ker = ↑{a | a ^ ((Nat.card K' - 1) / (Nat.card K - 1)) = 1}

Tactic:
;

Goal state after:
K : Type u_1
K' : Type u_2
inst✝³ : Field K
inst✝² : Field K'
inst✝¹ : Algebra K K'
inst✝ : Finite K'
this✝ : Finite K
this : Fintype K'ˣ
⊢ ↑(Units.map (Algebra.norm K)).ker = ↑{a | a ^ ((Nat.card K' - 1) / (Nat.card K - 1)) = 1}