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

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

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

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

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:
·

Goal state after:
case zero
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
⊢ (1 < x → 0 < eval x (cyclotomic 0 R)) ∧ (1 ≤ x → 0 ≤ eval x (cyclotomic 0 R))
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

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

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

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:
·

Goal state after:
case succ.zero
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
⊢ (1 < x → 0 < eval x (cyclotomic (0 + 1) R)) ∧ (1 ≤ x → 0 ≤ eval x (cyclotomic (0 + 1) R))
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

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

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:
·

Goal state after:
case succ.succ.zero
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
⊢ (1 < x → 0 < eval x (cyclotomic (0 + 1 + 1) R)) ∧ (1 ≤ x → 0 ≤ eval x (cyclotomic (0 + 1 + 1) R))
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Goal state before:
pp: R : Type u_1
p m : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hm : ¬p ∣ m
a : ℕ
x✝ : 0 < a + 2
hdiv : p ∣ p ^ a.succ * m
⊢ ¬p ∣ m

Tactic:
·

Goal state after:
R : Type u_1
p m : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hm : ¬p ∣ m
a : ℕ
x✝ : 0 < a + 2
hdiv : p ∣ p ^ a.succ * m
⊢ ¬p ∣ m
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Goal state before:
pp: case inl
m p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst✝ : NeZero ↑m
⊢ (cyclotomic (p ^ 0 * m) R).IsRoot μ ↔ IsPrimitiveRoot μ m

pp: case inr
m k p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst✝ : NeZero ↑m
hk : k > 0
⊢ (cyclotomic (p ^ k * m) R).IsRoot μ ↔ IsPrimitiveRoot μ m

Tactic:
·

Goal state after:
case inl
m p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst✝ : NeZero ↑m
⊢ (cyclotomic (p ^ 0 * m) R).IsRoot μ ↔ IsPrimitiveRoot μ m
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
p q : ℕ
x y : L
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hirr : Irreducible (cyclotomic (p.lcm q) K)
⊢ φ (p.lcm q) ≤ Module.finrank K L

Tactic:
rcases Nat.eq_zero_or_pos p with (rfl | hppos)

Goal state after:
case inl
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
q : ℕ
x y : L
hy : IsPrimitiveRoot y q
hx : IsPrimitiveRoot x 0
hirr : Irreducible (cyclotomic (Nat.lcm 0 q) K)
⊢ φ (Nat.lcm 0 q) ≤ Module.finrank K L

case inr
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
p q : ℕ
x y : L
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hirr : Irreducible (cyclotomic (p.lcm q) K)
hppos : p > 0
⊢ φ (p.lcm q) ≤ Module.finrank K L
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: case inl
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
q : ℕ
x y : L
hy : IsPrimitiveRoot y q
hx : IsPrimitiveRoot x 0
hirr : Irreducible (cyclotomic (Nat.lcm 0 q) K)
⊢ φ (Nat.lcm 0 q) ≤ Module.finrank K L

pp: case inr
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
p q : ℕ
x y : L
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hirr : Irreducible (cyclotomic (p.lcm q) K)
hppos : p > 0
⊢ φ (p.lcm q) ≤ Module.finrank K L

Tactic:
·

Goal state after:
case inl
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
q : ℕ
x y : L
hy : IsPrimitiveRoot y q
hx : IsPrimitiveRoot x 0
hirr : Irreducible (cyclotomic (Nat.lcm 0 q) K)
⊢ φ (Nat.lcm 0 q) ≤ Module.finrank K L
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_1
S T : Set ℕ
A : Type u
B : Type v
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ⇑(algebraMap B C)
n✝ : ℕ
hn : n✝ ∈ S ∪ T
⊢ n✝ ≠ 0 → ∃ r, IsPrimitiveRoot r n✝

pp: case refine_2
S T : Set ℕ
A : Type u
B : Type v
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ⇑(algebraMap B C)
x : C
⊢ x ∈ adjoin A {b | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1}

Tactic:
·

Goal state after:
case refine_1
S T : Set ℕ
A : Type u
B : Type v
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ⇑(algebraMap B C)
n✝ : ℕ
hn : n✝ ∈ S ∪ T
⊢ n✝ ≠ 0 → ∃ r, IsPrimitiveRoot r n✝
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:
·

Goal state after:
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))
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Goal state before:
pp: case inr.refine_1
m k p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst✝ : NeZero ↑m
hk : k > 0
h : (cyclotomic (p ^ k * m) R).IsRoot μ
⊢ IsPrimitiveRoot μ m

pp: case inr.refine_2
m k p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst✝ : NeZero ↑m
hk : k > 0
h : IsPrimitiveRoot μ m
⊢ (cyclotomic (p ^ k * m) R).IsRoot μ

Tactic:
·

Goal state after:
case inr.refine_1
m k p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst✝ : NeZero ↑m
hk : k > 0
h : (cyclotomic (p ^ k * m) R).IsRoot μ
⊢ IsPrimitiveRoot μ m
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: case inr.inl
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
p : ℕ
x y : L
hx : IsPrimitiveRoot x p
hppos : p > 0
hy : IsPrimitiveRoot y 0
hirr : Irreducible (cyclotomic (p.lcm 0) K)
⊢ φ (p.lcm 0) ≤ Module.finrank K L

pp: case inr.inr
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
p q : ℕ
x y : L
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hirr : Irreducible (cyclotomic (p.lcm q) K)
hppos : p > 0
hqpos : q > 0
⊢ φ (p.lcm q) ≤ Module.finrank K L

Tactic:
·

Goal state after:
case inr.inl
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
p : ℕ
x y : L
hx : IsPrimitiveRoot x p
hppos : p > 0
hy : IsPrimitiveRoot y 0
hirr : Irreducible (cyclotomic (p.lcm 0) K)
⊢ φ (p.lcm 0) ≤ Module.finrank K L
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
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ⇑(algebraMap B C)
n✝ : ℕ
hn' : n✝ ≠ 0
hn : n✝ ∈ S
⊢ ∃ r, IsPrimitiveRoot r n✝

pp: case refine_1.inr
S T : Set ℕ
A : Type u
B : Type v
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ⇑(algebraMap B C)
n✝ : ℕ
hn' : n✝ ≠ 0
hn : n✝ ∈ T
⊢ ∃ r, IsPrimitiveRoot r n✝

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
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ⇑(algebraMap B C)
n✝ : ℕ
hn' : n✝ ≠ 0
hn : n✝ ∈ S
⊢ ∃ r, IsPrimitiveRoot r n✝
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Goal state before:
pp: case inr.refine_2
m k p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst✝ : NeZero ↑m
hk : k > 0
h : IsPrimitiveRoot μ m
⊢ (cyclotomic (p ^ k * m) R).IsRoot μ

Tactic:
·

Goal state after:
case inr.refine_2
m k p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst✝ : NeZero ↑m
hk : k > 0
h : IsPrimitiveRoot μ m
⊢ (cyclotomic (p ^ k * m) R).IsRoot μ
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℕ
a✝ : 1 < x
⊢ 2 < n + 1 + 1 + 1

Tactic:
by lia

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℕ
a✝ : 1 ≤ x
⊢ 2 < n + 1 + 1 + 1

Tactic:
by lia

Goal state after:
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
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ⇑(algebraMap B C)
n✝ : ℕ
hn' : n✝ ≠ 0
hn : n✝ ∈ T
⊢ ∃ r, IsPrimitiveRoot r n✝

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
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ⇑(algebraMap B C)
n✝ : ℕ
hn' : n✝ ≠ 0
hn : n✝ ∈ T
⊢ ∃ r, IsPrimitiveRoot r n✝
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: case inl
R : Type u_1
inst✝ : Ring R
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ 0
⊢ eval 1 (cyclotomic 0 R) = 1

pp: case inr
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
⊢ eval 1 (cyclotomic n R) = 1

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝ : Ring R
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ 0
⊢ eval 1 (cyclotomic 0 R) = 1
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: case inr.inl
R : Type u_1
inst✝ : Ring R
n : ℕ
h✝ : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
h : eval 1 (cyclotomic n ℤ) = 1
⊢ eval 1 (cyclotomic n R) = 1

pp: case inr.inr
R : Type u_1
inst✝ : Ring R
n : ℕ
h✝ : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
h : eval 1 (cyclotomic n ℤ) = -1
⊢ eval 1 (cyclotomic n R) = 1

pp: R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
⊢ eval 1 (cyclotomic n ℤ) = 1 ∨ eval 1 (cyclotomic n ℤ) = -1

Tactic:
·

Goal state after:
case inr.inl
R : Type u_1
inst✝ : Ring R
n : ℕ
h✝ : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
h : eval 1 (cyclotomic n ℤ) = 1
⊢ eval 1 (cyclotomic n R) = 1
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_2
S T : Set ℕ
A : Type u
B : Type v
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ⇑(algebraMap B C)
x : C
⊢ x ∈ adjoin A {b | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1}

Tactic:
·

Goal state after:
case refine_2
S T : Set ℕ
A : Type u
B : Type v
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ⇑(algebraMap B C)
x : C
⊢ x ∈ adjoin A {b | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1}
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 ((X ^ Fintype.card K - X).rootSet K) = Algebra.adjoin F ↑(X ^ Fintype.card K - X).roots.toFinset

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 ↑(X ^ Fintype.card K - X).roots.toFinset = ⊤

Tactic:
·

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 ((X ^ Fintype.card K - X).rootSet K) = Algebra.adjoin F ↑(X ^ Fintype.card K - X).roots.toFinset
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 ↑(X ^ Fintype.card K - X).roots.toFinset = ⊤

Tactic:
·

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 ↑(X ^ Fintype.card K - X).roots.toFinset = ⊤
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝ : Ring R
n : ℕ
h✝ : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
h : eval 1 (cyclotomic n ℤ) = -1
⊢ eval 1 (cyclotomic n R) = 1

pp: R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
⊢ eval 1 (cyclotomic n ℤ) = 1 ∨ eval 1 (cyclotomic n ℤ) = -1

Tactic:
·

Goal state after:
case inr.inr
R : Type u_1
inst✝ : Ring R
n : ℕ
h✝ : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
h : eval 1 (cyclotomic n ℤ) = -1
⊢ eval 1 (cyclotomic n R) = 1
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this✝ : Fact (Nat.Prime p)
this :
  ↑n =
    (∏ x ∈ n.divisors.erase 1 \ image (fun t ↦ p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ)) *
      ∏ x ∈ range (padicValNat p n), eval 1 (cyclotomic (p ^ (x + 1)) ℤ)
⊢ False

pp: R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this✝ : Fact (Nat.Prime p)
this :
  ↑n =
    (∏ x ∈ n.divisors.erase 1 \ image (fun t ↦ p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ)) *
      ∏ x ∈ image (fun t ↦ p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ)
⊢ Set.InjOn (fun t ↦ p ^ (t + 1)) ↑(range (padicValNat p n))

Tactic:
·

Goal state after:
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this✝ : Fact (Nat.Prime p)
this :
  ↑n =
    (∏ x ∈ n.divisors.erase 1 \ image (fun t ↦ p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ)) *
      ∏ x ∈ range (padicValNat p n), eval 1 (cyclotomic (p ^ (x + 1)) ℤ)
⊢ False
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: case inl
n : ℕ
inst✝³ : NeZero n
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl✝ : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) n
r : ℕ
hr : GCDMonoid.lcm l n = n * r
ineq : φ n * φ r ≤ φ (GCDMonoid.lcm l n)
rpos : 0 < r
key : r = 1
⊢ l ∣ 2 * n

pp: case inr
n : ℕ
inst✝³ : NeZero n
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl✝ : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) n
r : ℕ
hr : GCDMonoid.lcm l n = n * r
ineq : φ n * φ r ≤ φ (GCDMonoid.lcm l n)
rpos : 0 < r
key : r = 2
⊢ l ∣ 2 * n

Tactic:
·

Goal state after:
case inl
n : ℕ
inst✝³ : NeZero n
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl✝ : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) n
r : ℕ
hr : GCDMonoid.lcm l n = n * r
ineq : φ n * φ r ≤ φ (GCDMonoid.lcm l n)
rpos : 0 < r
key : r = 1
⊢ l ∣ 2 * n
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this✝ : Fact (Nat.Prime p)
this :
  ↑n =
    ↑p ^ padicValNat p n *
      ∏ x ∈ n.divisors.erase 1 \ image (fun t ↦ p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ)
⊢ {n} ⊆ n.divisors.erase 1 \ image (fun t ↦ p ^ (t + 1)) (range (padicValNat p n))

pp: R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this✝ : Fact (Nat.Prime p)
this :
  ↑n =
    ↑p ^ padicValNat p n *
      ((∏ x ∈ (n.divisors.erase 1 \ image (fun t ↦ p ^ (t + 1)) (range (padicValNat p n))) \ {n},
          eval 1 (cyclotomic x ℤ)) *
        ∏ x ∈ {n}, eval 1 (cyclotomic x ℤ))
⊢ False

Tactic:
·

Goal state after:
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this✝ : Fact (Nat.Prime p)
this :
  ↑n =
    ↑p ^ padicValNat p n *
      ∏ x ∈ n.divisors.erase 1 \ image (fun t ↦ p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ)
⊢ {n} ⊆ n.divisors.erase 1 \ image (fun t ↦ p ^ (t + 1)) (range (padicValNat p n))
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: case inr
n : ℕ
inst✝³ : NeZero n
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl✝ : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) n
r : ℕ
hr : GCDMonoid.lcm l n = n * r
ineq : φ n * φ r ≤ φ (GCDMonoid.lcm l n)
rpos : 0 < r
key : r = 2
⊢ l ∣ 2 * n

Tactic:
·

Goal state after:
case inr
n : ℕ
inst✝³ : NeZero n
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl✝ : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) n
r : ℕ
hr : GCDMonoid.lcm l n = n * r
ineq : φ n * φ r ≤ φ (GCDMonoid.lcm l n)
rpos : 0 < r
key : r = 2
⊢ l ∣ 2 * n
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_1
S : Set ℕ
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Subsingleton B
this : Subsingleton (Subalgebra A B)
x✝ : IsCyclotomicExtension S A B
hprim : ∀ {n : ℕ}, n ∈ S → n ≠ 0 → ∃ r, IsPrimitiveRoot r n
adjoin_roots✝ : ∀ (x : B), x ∈ adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}
⊢ S ⊆ {0, 1}

pp: case refine_2
S : Set ℕ
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Subsingleton B
this : Subsingleton (Subalgebra A B)
hS : S ⊆ {0, 1}
⊢ IsCyclotomicExtension S A B

Tactic:
·

Goal state after:
case refine_1
S : Set ℕ
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Subsingleton B
this : Subsingleton (Subalgebra A B)
x✝ : IsCyclotomicExtension S A B
hprim : ∀ {n : ℕ}, n ∈ S → n ≠ 0 → ∃ r, IsPrimitiveRoot r n
adjoin_roots✝ : ∀ (x : B), x ∈ adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}
⊢ S ⊆ {0, 1}
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: n : ℕ
inst✝³ : NeZero n
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
⊢ 2 * n = orderOf (-1) * orderOf ζ

pp: n : ℕ
inst✝³ : NeZero n
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
⊢ (orderOf (-1)).Coprime (orderOf ζ)

Tactic:
·

Goal state after:
n : ℕ
inst✝³ : NeZero n
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
⊢ 2 * n = orderOf (-1) * orderOf ζ
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: n : ℕ
inst✝³ : NeZero n
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
⊢ (orderOf (-1)).Coprime (orderOf ζ)

Tactic:
·

Goal state after:
n : ℕ
inst✝³ : NeZero n
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
⊢ (orderOf (-1)).Coprime (orderOf ζ)
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_2
S : Set ℕ
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Subsingleton B
this : Subsingleton (Subalgebra A B)
hS : S ⊆ {0, 1}
⊢ IsCyclotomicExtension S A B

Tactic:
·

Goal state after:
case refine_2
S : Set ℕ
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Subsingleton B
this : Subsingleton (Subalgebra A B)
hS : S ⊆ {0, 1}
⊢ IsCyclotomicExtension S A B