mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

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

pp: case neg
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
hn : ¬n = 0
⊢ nthRootsFinset n 1 = n.divisors.biUnion fun i ↦ primitiveRoots i R

Tactic:
·

Goal state after:
case pos
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
hn : n = 0
⊢ nthRootsFinset n 1 = n.divisors.biUnion fun i ↦ primitiveRoots i R
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case h.inl
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
hk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic m K = cyclotomic' m K
ζ : K
hz : IsPrimitiveRoot ζ k
hzero : k = 0
⊢ cyclotomic k K = cyclotomic' k K

pp: case h.inr
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
hk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic m K = cyclotomic' m K
ζ : K
hz : IsPrimitiveRoot ζ k
hpos : k > 0
⊢ cyclotomic k K = cyclotomic' k K

Tactic:
·

Goal state after:
case h.inl
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
hk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic m K = cyclotomic' m K
ζ : K
hz : IsPrimitiveRoot ζ k
hzero : k = 0
⊢ cyclotomic k K = cyclotomic' k K
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: case inl
R : Type u_1
inst✝ : CommRing R
ζ : R
i : ℕ
h : (cyclotomic i R).IsRoot ζ
hi : i ∈ Nat.divisors 0
⊢ ζ ^ 0 = 1

pp: case inr
R : Type u_1
inst✝ : CommRing R
n : ℕ
ζ : R
i : ℕ
hi : i ∈ n.divisors
h : (cyclotomic i R).IsRoot ζ
hn : n > 0
⊢ ζ ^ n = 1

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝ : CommRing R
ζ : R
i : ℕ
h : (cyclotomic i R).IsRoot ζ
hi : i ∈ Nat.divisors 0
⊢ ζ ^ 0 = 1
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: n : ℕ
h : 0 < n
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
⊢ (∏ i ∈ n.divisors, cyclotomic i R).IsRoot ζ ↔ ∃ i ∈ n.divisors, (cyclotomic i R).IsRoot ζ

Tactic:
isRoot_prod

Goal state after:
n : ℕ
h : 0 < n
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
⊢ (∃ i ∈ n.divisors, (cyclotomic i R).IsRoot ζ) ↔ ∃ i ∈ n.divisors, (cyclotomic i R).IsRoot ζ
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
a✝ : Nontrivial R
hcycl : P = cyclotomic n R
⊢ P * ∏ i ∈ n.properDivisors, cyclotomic i R = X ^ n - 1

pp: case refine_2
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
a✝ : Nontrivial R
hP : P * ∏ i ∈ n.properDivisors, cyclotomic i R = X ^ n - 1
⊢ P = cyclotomic n R

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
a✝ : Nontrivial R
hcycl : P = cyclotomic n R
⊢ P * ∏ i ∈ n.properDivisors, cyclotomic i R = X ^ n - 1
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
a✝ : Nontrivial R
hcycl : P = cyclotomic n R
⊢ P * ∏ i ∈ n.properDivisors, cyclotomic i R = X ^ n - 1

pp: case refine_2
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
a✝ : Nontrivial R
hP : P * ∏ i ∈ n.properDivisors, cyclotomic i R = X ^ n - 1
⊢ P = cyclotomic n R

Tactic:
· rw [hcycl, ← prod_cyclotomic_eq_X_pow_sub_one hpos R, ← Nat.cons_self_properDivisors hpos.ne',
      Finset.prod_cons]

Goal state after:
case refine_2
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
a✝ : Nontrivial R
hP : P * ∏ i ∈ n.properDivisors, cyclotomic i R = X ^ n - 1
⊢ P = cyclotomic n R
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
a✝ : Nontrivial R
hP : P * ∏ i ∈ n.properDivisors, cyclotomic i R = X ^ n - 1
⊢ P = cyclotomic n R

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
a✝ : Nontrivial R
hP : P * ∏ i ∈ n.properDivisors, cyclotomic i R = X ^ n - 1
⊢ P = cyclotomic n R
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: case inl
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
h : (cyclotomic n R).roots = 0
⊢ (cyclotomic n R).roots.Nodup

pp: case inr
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
ζ : R
hζ : ζ ∈ (cyclotomic n R).roots
⊢ (cyclotomic n R).roots.Nodup

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
h : (cyclotomic n R).roots = 0
⊢ (cyclotomic n R).roots.Nodup
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
m : ℕ
hnm : cyclotomic 0 R = cyclotomic m R
⊢ 0 = m

pp: case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n m : ℕ
hnm : cyclotomic n R = cyclotomic m R
hzero : n ≠ 0
⊢ n = m

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
m : ℕ
hnm : cyclotomic 0 R = cyclotomic m R
⊢ 0 = m
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n m : ℕ
hnm : cyclotomic n R = cyclotomic m R
hzero : n ≠ 0
⊢ n = m

Tactic:
·

Goal state after:
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n m : ℕ
hnm : cyclotomic n R = cyclotomic m R
hzero : n ≠ 0
⊢ n = m
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: case inl
m : ℕ
h : 0 ≠ m
⊢ IsCoprime (cyclotomic 0 ℚ) (cyclotomic m ℚ)

pp: case inr
n m : ℕ
h : n ≠ m
hnzero : n > 0
⊢ IsCoprime (cyclotomic n ℚ) (cyclotomic m ℚ)

Tactic:
·

Goal state after:
case inl
m : ℕ
h : 0 ≠ m
⊢ IsCoprime (cyclotomic 0 ℚ) (cyclotomic m ℚ)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: case inr.inl
n : ℕ
hnzero : n > 0
h : n ≠ 0
⊢ IsCoprime (cyclotomic n ℚ) (cyclotomic 0 ℚ)

pp: case inr.inr
n m : ℕ
h : n ≠ m
hnzero : n > 0
hmzero : m > 0
⊢ IsCoprime (cyclotomic n ℚ) (cyclotomic m ℚ)

Tactic:
·

Goal state after:
case inr.inl
n : ℕ
hnzero : n > 0
h : n ≠ 0
⊢ IsCoprime (cyclotomic n ℚ) (cyclotomic 0 ℚ)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case pos
n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot : (cyclotomic n (ZMod p)).coeff 0 = 0
h : ↑a = 0
hone : n = 1
⊢ False

pp: case neg
n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot : (cyclotomic n (ZMod p)).coeff 0 = 0
h : ↑a = 0
hone : ¬n = 1
⊢ False

Tactic:
·

Goal state after:
case pos
n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot : (cyclotomic n (ZMod p)).coeff 0 = 0
h : ↑a = 0
hone : n = 1
⊢ False
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
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case refine_3
R : Type u_1
inst✝ : CommRing R
p : ℕ
hpri : Nat.Prime p
hp : p ≠ 2
a r : R
h₁ : r ∣ a ^ p
h₂ : r ∣ ↑p * a
this : C r ∣ (C a * X + -1) ^ p - (-1) ^ p
⊢ C r ∣ (C a * X - 1) ^ p + 1

pp: case refine_1
R : Type u_1
inst✝ : CommRing R
p : ℕ
hpri : Nat.Prime p
hp : p ≠ 2
a r : R
h₁ : r ∣ a ^ p
h₂ : r ∣ ↑p * a
⊢ C r ∣ (C a * X) ^ p

pp: case refine_2
R : Type u_1
inst✝ : CommRing R
p : ℕ
hpri : Nat.Prime p
hp : p ≠ 2
a r : R
h₁ : r ∣ a ^ p
h₂ : r ∣ ↑p * a
⊢ C r ∣ ↑p * (C a * X)

Tactic:
·

Goal state after:
case refine_3
R : Type u_1
inst✝ : CommRing R
p : ℕ
hpri : Nat.Prime p
hp : p ≠ 2
a r : R
h₁ : r ∣ a ^ p
h₂ : r ∣ ↑p * a
this : C r ∣ (C a * X + -1) ^ p - (-1) ^ p
⊢ C r ∣ (C a * X - 1) ^ p + 1
Module: Mathlib.RingTheory.Adjoin.PowerBasis

Goal state before:
pp: case hli
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ⇑(algebraMap (↥K[x]) S)
hx' : IsIntegral K ⟨x, ⋯⟩
⊢ LinearIndependent K fun i ↦ ⟨x, ⋯⟩ ^ ↑i

pp: case hsp
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ⇑(algebraMap (↥K[x]) S)
hx' : IsIntegral K ⟨x, ⋯⟩
⊢ ⊤ ≤ Submodule.span K (Set.range fun i ↦ ⟨x, ⋯⟩ ^ ↑i)

Tactic:
·

Goal state after:
case hli
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ⇑(algebraMap (↥K[x]) S)
hx' : IsIntegral K ⟨x, ⋯⟩
⊢ LinearIndependent K fun i ↦ ⟨x, ⋯⟩ ^ ↑i
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: case refine_1
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)
x✝ : cyclotomic p ℚ ∣ P
c : ℚ[X]
hc : P = cyclotomic p ℚ * c
⊢ ∀ (i j : Fin p), α i = α j

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 : ℕ
h : i < p
⊢ P.coeff i = (cyclotomic p ℚ * C (α 0)).coeff i

pp: case refine_3
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 : ℕ
h : ¬i < p
⊢ P.coeff i = (cyclotomic p ℚ * C (α 0)).coeff i

Tactic:
·

Goal state after:
case refine_1
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)
x✝ : cyclotomic p ℚ ∣ P
c : ℚ[X]
hc : P = cyclotomic p ℚ * c
⊢ ∀ (i j : Fin p), α i = α j
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommRing R
p : ℕ
hpri : Nat.Prime p
hp : p ≠ 2
a r : R
h₁ : r ∣ a ^ p
h₂ : r ∣ ↑p * a
⊢ C r ∣ (C a * X) ^ p

pp: case refine_2
R : Type u_1
inst✝ : CommRing R
p : ℕ
hpri : Nat.Prime p
hp : p ≠ 2
a r : R
h₁ : r ∣ a ^ p
h₂ : r ∣ ↑p * a
⊢ C r ∣ ↑p * (C a * X)

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommRing R
p : ℕ
hpri : Nat.Prime p
hp : p ≠ 2
a r : R
h₁ : r ∣ a ^ p
h₂ : r ∣ ↑p * a
⊢ C r ∣ (C a * X) ^ p
Module: Mathlib.RingTheory.Adjoin.PowerBasis

Goal state before:
pp: case hsp
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ⇑(algebraMap (↥K[x]) S)
hx' : IsIntegral K ⟨x, ⋯⟩
⊢ ⊤ ≤ Submodule.span K (Set.range fun i ↦ ⟨x, ⋯⟩ ^ ↑i)

Tactic:
·

Goal state after:
case hsp
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ⇑(algebraMap (↥K[x]) S)
hx' : IsIntegral K ⟨x, ⋯⟩
⊢ ⊤ ≤ Submodule.span K (Set.range fun i ↦ ⟨x, ⋯⟩ ^ ↑i)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case pos
n : ℕ
K : Type u_2
inst✝ : Field K
ζ x y : K
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hy : y = 0
⊢ x ^ n - y ^ n = ∏ ζ ∈ nthRootsFinset n 1, (x - ζ * y)

pp: case neg
n : ℕ
K : Type u_2
inst✝ : Field K
ζ x y : K
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hy : ¬y = 0
⊢ x ^ n - y ^ n = ∏ ζ ∈ nthRootsFinset n 1, (x - ζ * y)

Tactic:
·

Goal state after:
case pos
n : ℕ
K : Type u_2
inst✝ : Field K
ζ x y : K
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hy : y = 0
⊢ x ^ n - y ^ n = ∏ ζ ∈ nthRootsFinset n 1, (x - ζ * y)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case e'_2
n : ℕ
K : Type u_2
inst✝ : Field K
ζ x y : K
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hy : ¬y = 0
⊢ x ^ n - y ^ n = eval (x / y) (X ^ n - 1) * y ^ #(nthRootsFinset n 1)

pp: case e'_3
n : ℕ
K : Type u_2
inst✝ : Field K
ζ x y : K
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hy : ¬y = 0
⊢ ∏ ζ ∈ nthRootsFinset n 1, (x - ζ * y) = eval (x / y) (∏ ζ ∈ nthRootsFinset n 1, (X - C ζ)) * y ^ #(nthRootsFinset n 1)

Tactic:
·

Goal state after:
case e'_2
n : ℕ
K : Type u_2
inst✝ : Field K
ζ x y : K
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hy : ¬y = 0
⊢ x ^ n - y ^ n = eval (x / y) (X ^ n - 1) * y ^ #(nthRootsFinset n 1)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case e'_3
n : ℕ
K : Type u_2
inst✝ : Field K
ζ x y : K
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hy : ¬y = 0
⊢ ∏ ζ ∈ nthRootsFinset n 1, (x - ζ * y) = eval (x / y) (∏ ζ ∈ nthRootsFinset n 1, (X - C ζ)) * y ^ #(nthRootsFinset n 1)

Tactic:
·

Goal state after:
case e'_3
n : ℕ
K : Type u_2
inst✝ : Field K
ζ x y : K
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hy : ¬y = 0
⊢ ∏ ζ ∈ nthRootsFinset n 1, (x - ζ * y) = eval (x / y) (∏ ζ ∈ nthRootsFinset n 1, (X - C ζ)) * y ^ #(nthRootsFinset n 1)
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 : ℕ
h : i < p
⊢ P.coeff i = (cyclotomic p ℚ * C (α 0)).coeff i

pp: case refine_3
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 : ℕ
h : ¬i < 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 : ℕ
h : i < p
⊢ P.coeff i = (cyclotomic p ℚ * C (α 0)).coeff i
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: case refine_3
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 : ℕ
h : ¬i < p
⊢ P.coeff i = (cyclotomic p ℚ * C (α 0)).coeff i

Tactic:
·

Goal state after:
case refine_3
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 : ℕ
h : ¬i < p
⊢ P.coeff i = (cyclotomic p ℚ * C (α 0)).coeff i
Module: Mathlib.RingTheory.Adjoin.PowerBasis

Goal state before:
pp: case pos
S : Type u_2
inst✝⁶ : CommRing S
R : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
a✝ : Nontrivial S
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = (aeval B.gen) Q
hQ : Q = 0
⊢ IsIntegral R ((B.basis.repr (B.gen ^ n)) i)

pp: case neg
S : Type u_2
inst✝⁶ : CommRing S
R : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
a✝ : Nontrivial S
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = (aeval B.gen) Q
hQ : ¬Q = 0
⊢ IsIntegral R ((B.basis.repr (B.gen ^ n)) i)

Tactic:
·

Goal state after:
case pos
S : Type u_2
inst✝⁶ : CommRing S
R : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
a✝ : Nontrivial S
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = (aeval B.gen) Q
hQ : Q = 0
⊢ IsIntegral R ((B.basis.repr (B.gen ^ n)) i)
Module: Mathlib.RingTheory.Adjoin.PowerBasis

Goal state before:
pp: case pos
S : Type u_2
inst✝⁶ : CommRing S
R : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
a✝ : Nontrivial S
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = (aeval B.gen) Q
hQ : ¬Q = 0
hlt : Q.natDegree < B.dim
j : ℕ
hj : j < B.dim
hij : ⟨j, hj⟩ = i
⊢ IsIntegral R (Q.coeff j • if ⟨j, hj⟩ = i then 1 else 0)

pp: case neg
S : Type u_2
inst✝⁶ : CommRing S
R : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
a✝ : Nontrivial S
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = (aeval B.gen) Q
hQ : ¬Q = 0
hlt : Q.natDegree < B.dim
j : ℕ
hj : j < B.dim
hij : ¬⟨j, hj⟩ = i
⊢ IsIntegral R (Q.coeff j • if ⟨j, hj⟩ = i then 1 else 0)

Tactic:
·

Goal state after:
case pos
S : Type u_2
inst✝⁶ : CommRing S
R : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
a✝ : Nontrivial S
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = (aeval B.gen) Q
hQ : ¬Q = 0
hlt : Q.natDegree < B.dim
j : ℕ
hj : j < B.dim
hij : ⟨j, hj⟩ = i
⊢ IsIntegral R (Q.coeff j • if ⟨j, hj⟩ = i then 1 else 0)
Module: Mathlib.RingTheory.Adjoin.PowerBasis

Goal state before:
pp: case neg
S : Type u_2
inst✝⁶ : CommRing S
R : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
a✝ : Nontrivial S
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = (aeval B.gen) Q
hQ : ¬Q = 0
hlt : Q.natDegree < B.dim
j : ℕ
hj : j < B.dim
hij : ¬⟨j, hj⟩ = i
⊢ IsIntegral R (Q.coeff j • if ⟨j, hj⟩ = i then 1 else 0)

Tactic:
·

Goal state after:
case neg
S : Type u_2
inst✝⁶ : CommRing S
R : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
a✝ : Nontrivial S
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = (aeval B.gen) Q
hQ : ¬Q = 0
hlt : Q.natDegree < B.dim
j : ℕ
hj : j < B.dim
hij : ¬⟨j, hj⟩ = i
⊢ IsIntegral R (Q.coeff j • if ⟨j, hj⟩ = i then 1 else 0)
Module: Mathlib.RingTheory.Adjoin.PowerBasis

Goal state before:
pp: case refine_1
S : Type u_2
inst✝⁶ : CommRing S
R : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
x : A
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
a✝ : Nontrivial A
⊢ (∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)) → ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr (x ^ 0)) i)

pp: case refine_2
S : Type u_2
inst✝⁶ : CommRing S
R : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
x : A
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n✝ : ℕ
a✝ : Nontrivial A
n : ℕ
hn :
  ∀ m ≤ n,
    (∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)) → ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr (x ^ m)) i)
⊢ (∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)) →
    ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr (x ^ (n + 1))) i)

Tactic:
·

Goal state after:
case refine_1
S : Type u_2
inst✝⁶ : CommRing S
R : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
x : A
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
a✝ : Nontrivial A
⊢ (∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)) → ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr (x ^ 0)) i)
Module: Mathlib.RingTheory.Adjoin.PowerBasis

Goal state before:
pp: case pos
S : Type u_2
inst✝⁶ : CommRing S
R : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
x : A
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
a✝¹ : Nontrivial A
a✝ : ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)
i : Fin B.dim
h✝ : ⟨0, ⋯⟩ = i
⊢ IsIntegral R 1

pp: case neg
S : Type u_2
inst✝⁶ : CommRing S
R : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
x : A
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
a✝¹ : Nontrivial A
a✝ : ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)
i : Fin B.dim
h✝ : ¬⟨0, ⋯⟩ = i
⊢ IsIntegral R 0

Tactic:
·

Goal state after:
case pos
S : Type u_2
inst✝⁶ : CommRing S
R : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
x : A
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
a✝¹ : Nontrivial A
a✝ : ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)
i : Fin B.dim
h✝ : ⟨0, ⋯⟩ = i
⊢ IsIntegral R 1