mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: 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 η
hη : IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s))
HKη : K⟮η⟯ = K⟮η + 1⟯
H : K⟮η + 1⟯.toSubalgebra = K[η + 1]
⊢ IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s))

Tactic:
by

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

Goal state before:
pp: 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 η
hη : IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s))
⊢ IsCyclotomicExtension {p ^ (k - s + 1)} K ↥K⟮η⟯

Tactic:
by

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
x✝ : ↥(primitiveRoots n ℂ)
⊢ (q + 1).toNNReal ≠ 0

Tactic:
by

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

Goal state before:
pp: 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 η
hη : IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s))
this : IsCyclotomicExtension {p ^ (k - s + 1)} K ↥K⟮η⟯
⊢ IsPrimitiveRoot (η₁ + 1) (p ^ (k - s + 1))

Tactic:
by

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

Goal state before:
pp: S✝ : Set ℕ
n : ℕ
S : Set ℕ
a✝ : n ∉ S
hs✝ : S.Finite
H :
  ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [IsDomain B]
    [h₂ : IsCyclotomicExtension S A B], Module.Finite A B
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h₂ : IsCyclotomicExtension (insert n S) A B
hn : ¬n = 0
this✝ : IsCyclotomicExtension S A ↥(adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
this : Module.Finite A ↥(adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
⊢ Module.Finite (↥(adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})) B

Tactic:
by

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

Goal state before:
pp: S : Set ℕ
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h₁ : Finite ↑S
h₂ : IsCyclotomicExtension S A B
⊢ Module.Finite A B

Tactic:
by

Goal state after:
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
h : NumberField K
inst✝¹ : Finite ↑S
inst✝ : IsCyclotomicExtension S K L
⊢ FiniteDimensional ℚ L

Tactic:
by

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
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
ζ : ℂ
hζ : ζ ∈ primitiveRoots n ℂ
hhζ : ‖↑q - ζ‖ < q + 1
⊢ True ∧ ‖↑q - ζ‖ < ↑(q + 1).toNNReal

Tactic:
by

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

Goal state before:
pp: A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : IsDomain B
ζ : B
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
⊢ adjoin A ((cyclotomic n A).rootSet B) = adjoin A {b | ∃ a ∈ {n}, a ≠ 0 ∧ b ^ a = 1}

Tactic:
by

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

Goal state before:
pp: A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
n : ℕ
inst✝¹ : NeZero n
inst✝ : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ n
x : B
hx✝ : x ∈ (cyclotomic n A).rootSet B
hx : x ^ n = 1
⊢ x ∈ ↑A[ζ]

Tactic:
by

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

Goal state before:
pp: n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
⊢ eval q (cyclotomic n ℝ) < (q + 1) ^ φ n

Tactic:
by

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

Goal state before:
pp: q : ℝ
hq' : 1 < q
⊢ eval q (cyclotomic 0 ℝ) ≤ (q + 1) ^ φ 0

Tactic:
by

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

Goal state before:
pp: q : ℝ
hq' : 1 < q
⊢ eval q (cyclotomic 1 ℝ) ≤ (q + 1) ^ φ 1

Tactic:
by

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

Goal state before:
pp: q : ℝ
hq' : 1 < q
⊢ eval q (cyclotomic 2 ℝ) ≤ (q + 1) ^ φ 2

Tactic:
by

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

Goal state before:
pp: case refine_1
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
n : ℕ
inst✝¹ : NeZero n
inst✝ : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ n
x : B
hx : x ∈ (cyclotomic n A).rootSet B
⊢ x ∈ ↑A[ζ]

Tactic:
suffices hx : x ^ n = 1 by
      obtain ⟨i, _, rfl⟩ := hζ.eq_pow_of_pow_eq_one hx
      exact SetLike.mem_coe.2 (Subalgebra.pow_mem _ (subset_adjoin <| mem_singleton ζ) _)
    refine (isRoot_of_unity_iff (NeZero.pos n) B).2 ?_
    refine ⟨n, Nat.mem_divisors_self n (NeZero.ne n), ?_⟩
    rw [mem_rootSet', ← eval_map_algebraMap, map_cyclotomic, ← IsRoot] at hx
    exact hx.2

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

Goal state before:
pp: A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
n : ℕ
inst✝¹ : NeZero n
inst✝ : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ n
⊢ adjoin A ((cyclotomic n A).rootSet B) = A[ζ]

Tactic:
by

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

Goal state before:
pp: n q : ℕ
hn' : 1 < n
hq : q ≠ 1
⊢ (q - 1) ^ φ n < (eval (↑q) (cyclotomic n ℤ)).natAbs

Tactic:
by

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

Goal state before:
pp: A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
n : ℕ
inst✝¹ : NeZero n
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
ζ : B
hζ : IsPrimitiveRoot ζ n
⊢ A[ζ] = ⊤

Tactic:
by

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

Goal state before:
pp: A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
ζ : B
n : ℕ
inst✝ : NeZero n
h : IsPrimitiveRoot ζ n
n✝ : ℕ
hi : n✝ ∈ {n}
hi' : n✝ ≠ 0
⊢ ∃ r, IsPrimitiveRoot r n✝

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
inst✝¹ : Finite F
inst✝ : Algebra (ZMod (ringChar F)) F
a : F
ha : a ≠ 0
⊢ ∃ b, (Algebra.trace (ZMod (ringChar F)) F) (a * b) ≠ 0

Tactic:
by

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Finite L
inst✝ : Algebra K L
x : L
this✝ : Finite K
this : Fintype K
i : Fin (Module.finrank K L)
⊢ x ^ Nat.card K ^ ↑i = (frobeniusAlgEquivOfAlgebraic K L ^ ↑i) x

Tactic:
by

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Finite L
inst✝ : Algebra K L
x : L
⊢ (algebraMap K L) ((Algebra.trace K L) x) = ∑ i ∈ Finset.range (Module.finrank K L), x ^ Nat.card K ^ i

Tactic:
by

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Finite L
inst✝ : Algebra K L
x : L
⊢ (algebraMap K L) ((Algebra.norm K) x) = ∏ i ∈ Finset.range (Module.finrank K L), x ^ Nat.card K ^ i

Tactic:
by

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Finite L
inst✝ : Algebra K L
x : L
⊢ (algebraMap K L) ((Algebra.norm K) x) = x ^ ∑ i ∈ Finset.range (Module.finrank K L), Nat.card K ^ i

Tactic:
by

Goal state after:
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: n m d : ℕ
hm : n ∣ m
hd : m ∣ d
⊢ (unitsMap hm).comp (unitsMap hd) = unitsMap ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: n : ℕ
⊢ unitsMap ⋯ = MonoidHom.id (ZMod n)ˣ

Tactic:
by

Goal state after:
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: n m : ℕ
hm : NeZero m
h : n ∣ m
this : ∀ (x : ℕ), x.Coprime n → ∃ k, (x + k * n).Coprime m
⊢ Function.Surjective ⇑(unitsMap h)

Tactic:
by

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

Goal state before:
pp: A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
ζ : B
n : ℕ
inst✝ : NeZero n
h : IsPrimitiveRoot ζ n
x✝ : ↥A[ζ]
x : B
hx : x ∈ A[ζ]
⊢ ⟨x, hx⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}

Tactic:
by

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

Goal state before:
pp: K : Type w
L : Type z
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsIntegral K L
n : ℕ
inst✝ : NeZero n
ζ : L
hζ : IsPrimitiveRoot ζ n
⊢ IsCyclotomicExtension {n} K ↥K⟮ζ⟯

Tactic:
by

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

Goal state before:
pp: n : ℕ
inst✝³ : NeZero n
S : Set ℕ
K : Type w
L : Type z
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : IsCyclotomicExtension S K L
hS : n ∈ S
⊢ (map (algebraMap K L) (X ^ n - 1)).Splits

Tactic:
by

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

Goal state before:
pp: n : ℕ
inst✝⁴ : NeZero n
S : Set ℕ
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension S K L
hS : n ∈ S
⊢ cyclotomic n K ∣ X ^ n - 1

Tactic:
use ∏ i ∈ n.properDivisors, Polynomial.cyclotomic i K

Goal state after:
case h
n : ℕ
inst✝⁴ : NeZero n
S : Set ℕ
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension S K L
hS : n ∈ S
⊢ X ^ n - 1 = cyclotomic n K * ∏ i ∈ n.properDivisors, cyclotomic i K
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
inst✝⁴ : NeZero n
S : Set ℕ
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension S K L
hS : n ∈ S
⊢ (map (algebraMap K L) (cyclotomic n K)).Splits

Tactic:
by

Goal state after:
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
h : ∀ n ∈ S, n ≠ 0 → ∃ r, IsPrimitiveRoot r n
b : L
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
h2 : b ^ n = 1
⊢ (aeval b) (X ^ n - 1) = 0

Tactic:
by

Goal state after:
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
h : ∀ n ∈ S, n ≠ 0 → ∃ r, IsPrimitiveRoot r n
⊢ ∀ b ∈ {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}, IsAlgebraic K b

Tactic:
by

Goal state after:
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: n m : ℕ
hm : NeZero m
h : n ∣ m
⊢ Function.Surjective ⇑(unitsMap h)

Tactic:
by

Goal state after:
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: n p : ℕ
h : p ∈ n.primeFactors
⊢ ¬IsUnit ↑p

Tactic:
by

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

Goal state before:
pp: 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) η₁ = ↑(p ^ (k - s + 1)).minFac
this : p ^ ((k - s).succ - 1) * Module.finrank (↥K⟮η⟯) L = p ^ (k.succ - 1)
⊢ k.succ - 1 = (k - s).succ - 1 + s

Tactic:
by

Goal state after:
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: ⊢ 0 = 1 * ↑0

Tactic:
by

Goal state after:
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
h : ∀ n ∈ S, n ≠ 0 → ∃ r, IsPrimitiveRoot r n
⊢ IsCyclotomicExtension S K ↥(IntermediateField.adjoin K {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})

Tactic:
by

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

Goal state before:
pp: 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
⊢ (Algebra.norm K) (ζ ^ p ^ s - 1) = ↑p ^ p ^ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
⊢ IsUnit ↑a₀

Tactic:
by

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

Goal state before:
pp: p : ℕ
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
s : ℕ
hs : s ≤ k
hodd : p ≠ 2
⊢ (Algebra.norm K) (ζ ^ p ^ s - 1) = ↑p ^ p ^ s

Tactic:
by

Goal state after:
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
this✝¹ : Algebra.IsIntegral K L
h : (IntermediateField.adjoin K {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}).toSubalgebra = ⊤.toSubalgebra
b : L
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
h2 : b ^ n = 1
this✝ : NeZero n
this : (X ^ n - 1).Separable
⊢ (aeval b) (X ^ n - 1) = 0

Tactic:
by

Goal state after:
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
⊢ Algebra.IsSeparable K L

Tactic:
by

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

Goal state before:
pp: p : ℕ
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
h : p ≠ 2
⊢ (Algebra.norm K) (ζ - 1) = ↑p

Tactic:
by

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

Goal state before:
pp: p : ℕ
K : Type u
L : Type v
inst✝² : Field L
ζ : L
inst✝¹ : Field K
inst✝ : Algebra K L
hpri : Fact (Nat.Prime p)
hcyc : IsCyclotomicExtension {p} K L
hζ : IsPrimitiveRoot ζ p
hirr : Irreducible (cyclotomic p K)
h : p ≠ 2
⊢ Irreducible (cyclotomic (p ^ (0 + 1)) K)

Tactic:
by

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

Goal state before:
pp: p : ℕ
K : Type u
L : Type v
inst✝² : Field L
ζ : L
inst✝¹ : Field K
inst✝ : Algebra K L
hpri : Fact (Nat.Prime p)
hcyc : IsCyclotomicExtension {p} K L
hζ : IsPrimitiveRoot ζ p
h : p ≠ 2
hirr : Irreducible (cyclotomic (p ^ (0 + 1)) K)
⊢ IsPrimitiveRoot ζ (p ^ (0 + 1))

Tactic:
by

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

Goal state before:
pp: p : ℕ
K : Type u
L : Type v
inst✝² : Field L
ζ : L
inst✝¹ : Field K
inst✝ : Algebra K L
hpri : Fact (Nat.Prime p)
hcyc : IsCyclotomicExtension {p} K L
h : p ≠ 2
hirr : Irreducible (cyclotomic (p ^ (0 + 1)) K)
hζ : IsPrimitiveRoot ζ (p ^ (0 + 1))
⊢ IsCyclotomicExtension {p ^ (0 + 1)} K L

Tactic:
by

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

Goal state before:
pp: p : ℕ
K : Type u
L : Type v
inst✝² : Field L
ζ : L
inst✝¹ : Field K
inst✝ : Algebra K L
hpri : Fact (Nat.Prime p)
hcyc : IsCyclotomicExtension {p} K L
hζ : IsPrimitiveRoot ζ p
hirr : Irreducible (cyclotomic p K)
h : p ≠ 2
⊢ (Algebra.norm K) (ζ - 1) = ↑p

Tactic:
by

Goal state after:
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: N : ℕ
a : ZMod N
⊢ ∃ d, d ∣ N ∧ ∃ u, IsUnit u ∧ a = u * ↑d

Tactic:
by

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

Goal state before:
pp: K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (2 ^ (k + 1)) K)
this : IsPrimitiveRoot (ζ ^ 2 ^ k) 2
⊢ -1 - 1 = (algebraMap K L) (-2)

Tactic:
by

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

Goal state before:
pp: K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (2 ^ (k + 1)) K)
this : IsPrimitiveRoot (ζ ^ 2 ^ k) 2
H : -1 - 1 = (algebraMap K L) (-2)
⊢ Irreducible (cyclotomic (2 ^ (k + 1)) K)

Tactic:
by

Goal state after:
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: n : ℕ
x : ℤ
h : IsCoprime x ↑n
⊢ ↑x * (↑x)⁻¹ = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: n : ℕ
x : ℤ
h : IsCoprime x ↑n
⊢ (↑x)⁻¹ * ↑x = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
m : ℤ
h : IsCoprime m ↑n
⊢ ↑m * ↑(↑m)⁻¹.val = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
m : ℤ
h : IsCoprime m ↑n
⊢ ↑(↑m)⁻¹.val * ↑m = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: m : ℕ
n : ℤ
h : IsUnit ↑n
⊢ IsUnit (↑n)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: n : ℤ
m : ℕ
h : IsCoprime (↑m) n
⊢ ↑(unitOfIsCoprime n ⋯) = ↑n

Tactic:
by

Goal state after:
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} = ⊤
y : L
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
h2 : y ^ n = 1
⊢ i y ^ n = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: n : ℤ
m : ℕ
⊢ IsUnit ↑n ↔ IsCoprime (↑m) n

Tactic:
by

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

Goal state before:
pp: K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (2 ^ (k + 1)) K)
⊢ (Algebra.norm K) (ζ ^ 2 ^ k - 1) = (-2) ^ 2 ^ k

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommMonoid R'
φ : AddChar R R'
a : R
h : 0 < ringChar R
⊢ ⋯.unit ∈ rootsOfUnity (↑(ringChar R).toPNat') R'

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommMonoid R'
R'' : Type u_1
inst✝ : CommMonoid R''
φ : AddChar R R'
f : R' →* R''
hφ : φ.IsPrimitive
hf : Function.Injective ⇑f
a : R
ha : a ≠ 0
⊢ (f.compAddChar φ).mulShift a ≠ 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommMonoid R'
ψ : AddChar R R'
hψ : ψ.IsPrimitive
⊢ Function.Injective ψ.mulShift

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: R' : Type v
inst✝¹ : CommMonoid R'
F : Type u
inst✝ : Field F
ψ : AddChar F R'
hψ : ψ ≠ 1
a : F
ha : a ≠ 0
h : ψ.mulShift a = 1
⊢ ψ = 1

Tactic:
by

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

Goal state before:
pp: K : Type u
L : Type v
inst✝² : Field L
ζ : L
inst✝¹ : Field K
inst✝ : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (2 ^ k)
hk : 2 ≤ k
H : IsCyclotomicExtension {2 ^ k} K L
hirr : Irreducible (cyclotomic (2 ^ k) K)
⊢ 2 < 2 ^ k

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommMonoid R'
inst✝ : Finite R
e : AddChar R R'
r x : R
h : x * r = 0
h' : ¬x = 0
⊢ ¬(e.mulShift r).mulShift x ≠ 1

Tactic:
by

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

Goal state before:
pp: K : Type u
L : Type v
inst✝² : Field L
ζ : L
inst✝¹ : Field K
inst✝ : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (2 ^ k)
hk : 2 ≤ k
H : IsCyclotomicExtension {2 ^ k} K L
hirr : Irreducible (cyclotomic (2 ^ k) K)
this : 2 < 2 ^ k
⊢ Irreducible (cyclotomic (2 ^ k) K)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommMonoid R'
inst✝ : Finite R
e : AddChar R R'
r : R
hr : ¬IsUnit r
⊢ ¬(e.mulShift r).IsPrimitive

Tactic:
by

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

Goal state before:
pp: K : Type u
L : Type v
inst✝² : Field L
ζ : L
inst✝¹ : Field K
inst✝ : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (2 ^ k)
hk : 2 ≤ k
H : IsCyclotomicExtension {2 ^ k} K L
this : 2 < 2 ^ k
hirr : Irreducible (cyclotomic (2 ^ k) K)
⊢ IsPrimitiveRoot ζ (2 ^ k)

Tactic:
by

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

Goal state before:
pp: p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
⊢ Module.finrank (ZMod p) (GaloisField p n) = n

Tactic:
by

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

Goal state before:
pp: K : Type u
L : Type v
inst✝² : Field L
ζ : L
inst✝¹ : Field K
inst✝ : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (2 ^ k)
hk : 2 ≤ k
H : IsCyclotomicExtension {2 ^ k} K L
hirr : Irreducible (cyclotomic (2 ^ k) K)
⊢ (Algebra.norm K) (ζ - 1) = 2

Tactic:
by

Goal state after:
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
⊢ Nonempty (L ≃ₐ[K] ↥(IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: N : ℕ
inst✝¹ : NeZero N
R : Type u_1
inst✝ : CommRing R
e : AddChar (ZMod N) R
d : ℕ
hd : d ∣ N
u : ZMod N
hu : IsUnit u
hb_ne : u * ↑d ≠ 0
hb : e.mulShift (u * ↑d) = 1
h : d = N
⊢ False

Tactic:
by

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

Goal state before:
pp: p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
⊢ Nat.card (GaloisField p n) = p ^ n

Tactic:
by

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

Goal state before:
pp: p : ℕ
h_prime : Fact (Nat.Prime p)
hp : 1 < p
⊢ (X ^ p - X).roots = univ.val

Tactic:
by

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

Goal state before:
pp: p : ℕ
h_prime : Fact (Nat.Prime p)
⊢ (X ^ p - X).Splits

Tactic:
by

Goal state after: