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

Goal state before:
pp: case pos
n : ℕ
hzero : n = 0
⊢ map (Int.castRingHom ℂ) (cyclotomic n ℤ) = cyclotomic' n ℂ ∧
    (cyclotomic n ℤ).degree = (cyclotomic' n ℂ).degree ∧ (cyclotomic n ℤ).Monic

Tactic:
simp only [hzero, cyclotomic, degree_one, monic_one, cyclotomic'_zero, dif_pos,
      Polynomial.map_one, and_self_iff]

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

Goal state before:
pp: n : ℕ
⊢ map (Int.castRingHom ℂ) (cyclotomic n ℤ) = cyclotomic' n ℂ ∧
    (cyclotomic n ℤ).degree = (cyclotomic' n ℂ).degree ∧ (cyclotomic n ℤ).Monic

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ ξ : Rˣ
h : IsPrimitiveRoot ζ k
hξ : ξ ∈ rootsOfUnity k R
⊢ ∃ i < k, ζ ^ i = ξ

Tactic:
by

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

Goal state before:
pp: n : ℕ
P : ℤ[X]
h : map (Int.castRingHom ℂ) P = cyclotomic' n ℂ
⊢ P = cyclotomic n ℤ

Tactic:
apply map_injective (Int.castRingHom ℂ) Int.cast_injective
  rw [h, (int_cyclotomic_spec n).1]

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

Goal state before:
pp: n : ℕ
P : ℤ[X]
h : map (Int.castRingHom ℂ) P = cyclotomic' n ℂ
⊢ P = cyclotomic n ℤ

Tactic:
by

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

Goal state before:
pp: n : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
⊢ map f (cyclotomic n R) = cyclotomic n S

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ ξ : R
h : IsPrimitiveRoot ζ k
hξ : ξ ^ k = 1
⊢ ∃ i < k, ζ ^ i = ξ

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
q : R
n : ℕ
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
⊢ eval (f q) (cyclotomic n S) = f (eval q (cyclotomic n R))

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
⊢ cyclotomic 0 R = 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
⊢ map (Int.castRingHom ℂ) (X - 1) = cyclotomic' 1 ℂ

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
⊢ cyclotomic 1 R = X - 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : Ring R
⊢ (cyclotomic n R).Monic

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.Minpoly

Goal state before:
pp: case refine_1
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : P.Monic
Qmonic : Q.Monic
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : (P * Q).IsPrimitive
aux : Irreducible P ↔ Irreducible (map (Int.castRingHom ℚ) P)
⊢ ¬map (Int.castRingHom ℚ) P ∣ map (Int.castRingHom ℚ) Q

Tactic:
rw [map_dvd_map (Int.castRingHom ℚ) Int.cast_injective Pmonic]

Goal state after:
case refine_1
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : P.Monic
Qmonic : Q.Monic
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : (P * Q).IsPrimitive
aux : Irreducible P ↔ Irreducible (map (Int.castRingHom ℚ) P)
⊢ ¬P ∣ Q
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ ξ : Rˣ
h : IsPrimitiveRoot ζ k
⊢ IsPrimitiveRoot ξ k ↔ ∃ i < k, i.Coprime k ∧ ζ ^ i = ξ

Tactic:
by

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ (cyclotomic n R).degree = ↑n.totient

Tactic:
by

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ (cyclotomic n R).natDegree = n.totient

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma

Goal state before:
pp: E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
hf1 :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf2 : HasCompactSupport f
ε : ℝ
hε : ε > 0
R : ℝ
hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0
A : Set V := {v | ‖v‖ ≤ R + 1}
mA : MeasurableSet A
B : ℝ≥0
hB_pos : 0 < B
hB_vol : volume A ≤ ↑B
δ : ℝ
hδ1 : δ > 0
hδ2 : ∀ ⦃a b : V⦄, dist a b < δ → dist (f a) (f b) < ε / ↑B
w : V
hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖
hw_ne : w ≠ 0
hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)
this : ‖1 / 2‖ = 2⁻¹
⊢ ∀ v ∈ A, ‖‖f v - f (v + i w)‖‖ ≤ ε / ↑B

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n : ℕ
⊢ (cyclotomic n R).natDegree ≤ n.totient

Tactic:
by

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

Goal state before:
pp: n : ℕ
R : Type u_1
hpos : 0 < n
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ 0 < (cyclotomic n R).degree

Tactic:
by

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

Goal state before:
pp: n : ℕ
hpos : 0 < n
R : Type u_1
inst✝ : CommRing R
⊢ ∏ i ∈ n.divisors, cyclotomic i ℤ = X ^ n - 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ ξ : R
h : IsPrimitiveRoot ζ k
⊢ IsPrimitiveRoot ξ k ↔ ∃ i < k, i.Coprime k ∧ ζ ^ i = ξ

Tactic:
by

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

Goal state before:
pp: n : ℕ
hpos : 0 < n
R : Type u_1
inst✝ : CommRing R
⊢ ∏ i ∈ n.divisors, cyclotomic i R = X ^ n - 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : Ring R
this : cyclotomic n ℤ ∣ X ^ n - 1
⊢ cyclotomic n R ∣ X ^ n - 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : Ring R
⊢ cyclotomic n R ∣ X ^ n - 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.Minpoly

Goal state before:
pp: n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : P.Monic
Qmonic : Q.Monic
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : (P * Q).IsPrimitive
⊢ P * Q ∣ X ^ n - 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
h : 0 < n
R : Type u_1
inst✝ : CommRing R
this : ∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ = ∑ i ∈ range n, X ^ i
⊢ ∏ i ∈ n.divisors.erase 1, cyclotomic i R = ∑ i ∈ range n, X ^ i

Tactic:
by

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

Goal state before:
pp: n : ℕ
h : 0 < n
R : Type u_1
inst✝ : CommRing R
⊢ ∏ i ∈ n.divisors.erase 1, cyclotomic i R = ∑ i ∈ range n, X ^ i

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : ℕ
hp : Fact (Nat.Prime p)
this : cyclotomic p ℤ = ∑ i ∈ range p, X ^ i
⊢ cyclotomic p R = ∑ i ∈ range p, X ^ i

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : ℕ
hp : Fact (Nat.Prime p)
⊢ cyclotomic p R = ∑ i ∈ range p, X ^ i

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : ℕ
hn : Fact (Nat.Prime p)
⊢ cyclotomic p R * (X - 1) = X ^ p - 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
⊢ cyclotomic 2 R = X + 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
⊢ cyclotomic 3 R = X ^ 2 + X + 1

Tactic:
simp [cyclotomic_prime, sum_range_succ']

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
⊢ cyclotomic 3 R = X ^ 2 + X + 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
d n : ℕ
hdn : d ∣ n
hd : d ≠ 1
this : cyclotomic d ℤ ∣ ∑ i ∈ range n, X ^ i
⊢ cyclotomic d R ∣ ∑ i ∈ range n, X ^ i

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
d n : ℕ
hdn : d ∣ n
hd : d ≠ 1
⊢ cyclotomic d R ∣ ∑ i ∈ range n, X ^ i

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
d n : ℕ
hdvd : d ∣ n
hn : n ≠ 0
⊢ 0 < n

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
d n : ℕ
hdvd : d ∣ n
hn : n ≠ 0
h0d : 0 < d
⊢ 0 < n

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
d n : ℕ
hdvd : d ∣ n
hn : n ≠ 0
h0d : 0 < d
⊢ d.divisors ⊆ n.divisors

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
d n : ℕ
hdvd : d ∣ n
hn : n ≠ 0
⊢ (X ^ d - 1) * ∏ x ∈ n.divisors \ d.divisors, cyclotomic x R = X ^ n - 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
⊢ nthRoots n a = Multiset.map (fun x ↦ ζ ^ x * α) (Multiset.range n)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ n.properDivisors
⊢ (X ^ d - 1) * cyclotomic n R ∣ X ^ n - 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ (algebraMap R[X] (RatFunc R)) (cyclotomic n R) =
    ∏ i ∈ n.divisorsAntidiagonal, (algebraMap R[X] (RatFunc R)) (X ^ i.2 - 1) ^ μ i.1

Tactic:
rcases n.eq_zero_or_pos with (rfl | hpos)

Goal state after:
case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ (algebraMap R[X] (RatFunc R)) (cyclotomic 0 R) =
    ∏ i ∈ Nat.divisorsAntidiagonal 0, (algebraMap R[X] (RatFunc R)) (X ^ i.2 - 1) ^ μ i.1

case inr
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hpos : n > 0
⊢ (algebraMap R[X] (RatFunc R)) (cyclotomic n R) =
    ∏ i ∈ n.divisorsAntidiagonal, (algebraMap R[X] (RatFunc R)) (X ^ i.2 - 1) ^ μ i.1
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hpos : n > 0
⊢ ∀ (n : ℕ),
    0 < n → ∏ i ∈ n.divisors, (algebraMap R[X] (RatFunc R)) (cyclotomic i R) = (algebraMap R[X] (RatFunc R)) (X ^ n - 1)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.Minpoly

Goal state before:
pp: n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : P.Monic
Qmonic : Q.Monic
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : (P * Q).IsPrimitive
R : (ZMod p)[X]
prod : map (Int.castRingHom (ZMod p)) P ^ 2 * R ∣ X ^ n - 1
hR : map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) = map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) * R
⊢ map (Int.castRingHom (ZMod p)) P ^ 2 ∣ map (Int.castRingHom (ZMod p)) P ^ 2 * R

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
inst✝³ : CommRing R
inst✝² : IsDomain R
S : Type u_7
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
ζ₁ ζ₂ : R
k₁ k₂ : ℕ
hζ₁ : IsPrimitiveRoot ζ₁ k₁
hζ₂ : IsPrimitiveRoot ζ₂ k₂
hk₁ : k₁ ≠ 0
hk₂ : k₂ ≠ 0
ζ : R
hζ : IsPrimitiveRoot ζ (k₁.lcm k₂)
⊢ S[ζ₁, ζ₂] = S[ζ]

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.Minpoly

Goal state before:
pp: case neg
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : P.Monic
Qmonic : Q.Monic
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : (P * Q).IsPrimitive
R : (ZMod p)[X]
prod : map (Int.castRingHom (ZMod p)) P ^ 2 * R ∣ X ^ n - 1
hR : map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) = map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) * R
⊢ False

Tactic:
have habs : map (Int.castRingHom (ZMod p)) P ^ 2 ∣ map (Int.castRingHom (ZMod p)) P ^ 2 * R := by
    use R

Goal state after:
case neg
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : P.Monic
Qmonic : Q.Monic
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : (P * Q).IsPrimitive
R : (ZMod p)[X]
prod : map (Int.castRingHom (ZMod p)) P ^ 2 * R ∣ X ^ n - 1
hR : map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) = map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) * R
habs : map (Int.castRingHom (ZMod p)) P ^ 2 ∣ map (Int.castRingHom (ZMod p)) P ^ 2 * R
⊢ False
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
a : R
⊢ (nthRoots n a).card = if ∃ α, α ^ n = a then n else 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
inst✝² : CommRing R
ζ : Rˣ
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
h : IsPrimitiveRoot ζ n
⊢ Nat.card ↥(rootsOfUnity n R) = n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
ζ : R
n : ℕ
inst✝ : NeZero n
h : IsPrimitiveRoot ζ n
⊢ Nat.card ↥(rootsOfUnity n R) = n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
⊢ Nat.card ↥(rootsOfUnity n R) = n ↔ ∃ ζ, IsPrimitiveRoot ζ n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ (nthRoots n 1).card = n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
a : R
ha : a ≠ 0
hn : n > 0
α : R
hα : α ^ n = a
hα' : α = 0
⊢ a = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h✝ : IsPrimitiveRoot ζ n
a : R
ha : a ≠ 0
hn : n > 0
h : ∀ (α : R), α ^ n ≠ a
this : nthRoots n a = 0
⊢ (nthRoots n a).Nodup

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
a : R
ha : a ≠ 0
⊢ (nthRoots n a).Nodup

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ #(nthRootsFinset n 1) = n

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma

Goal state before:
pp: E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
hf1 :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf2 : HasCompactSupport f
⊢ Tendsto (fun w ↦ ∫ (v : V), 𝐞 (-⟪v, w⟫) • f v) (cocompact V) (𝓝 0)

Tactic:
by

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ (algebraMap R[X] (RatFunc R)) (cyclotomic n R) =
    ∏ i ∈ n.divisorsAntidiagonal, (algebraMap R[X] (RatFunc R)) (X ^ i.2 - 1) ^ μ i.1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.Minpoly

Goal state before:
pp: n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
⊢ minpoly ℤ μ = minpoly ℤ (μ ^ p)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
⊢ #(primitiveRoots k R) = φ k

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k l : ℕ
inst✝¹ : CommRing R
ζ : Rˣ
h✝ : IsPrimitiveRoot ζ k
inst✝ : IsDomain R
a b n : ℕ
h : a * b ≡ 1 [MOD n]
x : ↥(primitiveRoots n R)
⊢ 0 < n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k l : ℕ
inst✝¹ : CommRing R
ζ : Rˣ
h✝ : IsPrimitiveRoot ζ k
inst✝ : IsDomain R
a b n : ℕ
h : a * b ≡ 1 [MOD n]
x : ↥(primitiveRoots n R)
hr : 0 < n
⊢ a.Coprime n

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
a✝ : Nontrivial R
⊢ (∏ i ∈ n.properDivisors, cyclotomic i R).Monic

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma

Goal state before:
pp: E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
hfi : Integrable f volume
ε : ℝ
hε : ε > 0
g : V → E
hg_supp : HasCompactSupport g
hfg : ∫ (x : V), ‖f x - g x‖ ≤ ε / 2
hg_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
w : V
hI : ‖(∫ (v : V), 𝐞 (-⟪v, w⟫) • g v) - 0‖ < ε / 2
⊢ ‖(∫ (v : V), 𝐞 (-⟪v, w⟫) • f v) - ∫ (v : V), 𝐞 (-⟪v, w⟫) • g v‖ ≤ ε / 2

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k l : ℕ
inst✝¹ : CommRing R
ζ : Rˣ
h✝ : IsPrimitiveRoot ζ k
inst✝ : IsDomain R
a b n : ℕ
h : a * b ≡ 1 [MOD n]
x : ↥(primitiveRoots n R)
hr : 0 < n
⊢ b.Coprime n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k l : ℕ
inst✝¹ : CommRing R
ζ : Rˣ
h✝ : IsPrimitiveRoot ζ k
inst✝ : IsDomain R
a b n : ℕ
h : a * b ≡ 1 [MOD n]
x : ↥(primitiveRoots n R)
⊢ (fun x ↦ ⟨↑x ^ b, ⋯⟩) ((fun x ↦ ⟨↑x ^ a, ⋯⟩) x) = x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k l : ℕ
inst✝¹ : CommRing R
ζ : Rˣ
h✝ : IsPrimitiveRoot ζ k
inst✝ : IsDomain R
a b n : ℕ
h : a * b ≡ 1 [MOD n]
x : ↥(primitiveRoots n R)
⊢ (fun x ↦ ⟨↑x ^ a, ⋯⟩) ((fun x ↦ ⟨↑x ^ b, ⋯⟩) x) = x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁵ : CommMonoid M
inst✝⁴ : CommMonoid N
inst✝³ : DivisionCommMonoid G
k l : ℕ
inst✝² : CommRing R
ζ : Rˣ
h✝ : IsPrimitiveRoot ζ k
inst✝¹ : IsDomain R
a n : ℕ
h : a.Coprime n
inst✝ : NeZero n
h2 : ∃ m < n, a * m % n = 1 % n
⊢ a * h2.choose ≡ 1 [MOD n]

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
n : ℕ
inst✝ : NeZero n
x : R
this : x ^ n = 1 ↔ ∃ a, a ∣ n ∧ x ∈ primitiveRoots a R
⊢ x ∈ nthRootsFinset n 1 ↔ x ∈ n.divisors.biUnion fun i ↦ primitiveRoots i R

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
n : ℕ
inst✝ : NeZero n
x : R
a : ℕ
ha : x ∈ primitiveRoots a R
d : ℕ
hd : n = a * d
ha₀ : a = 0
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.Minpoly

Goal state before:
pp: n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
m : ℕ
hcop : m.Coprime n
⊢ minpoly ℤ μ = minpoly ℤ (μ ^ m)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma

Goal state before:
pp: E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
⊢ Tendsto (fun w ↦ ∫ (v : V), 𝐞 (-⟪v, w⟫) • f v) (cocompact V) (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.Minpoly

Goal state before:
pp: n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
m : ℕ
hcop : m.Coprime n
⊢ (map (Int.castRingHom K) (minpoly ℤ μ)).IsRoot (μ ^ m)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
⊢ Tendsto (fun w ↦ ∫ (v : ℝ), 𝐞 (-(v * w)) • f v) (cocompact ℝ) (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
n : ℕ
inst✝ : NeZero n
⊢ nthRootsFinset n 1 = n.divisors.biUnion fun i ↦ primitiveRoots i R

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
⊢ cyclotomic n R = (X ^ n - 1) /ₘ ∏ i ∈ n.properDivisors, cyclotomic i R

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
⊢ nthRootsFinset n 1 = n.divisors.biUnion fun i ↦ primitiveRoots i R

Tactic:
by

Goal state after: