K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ cyclotomic' n K ∈ lifts (Int.castRingHom K)
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ ∃ P, map (Int.castRingHom K) P = cyclotomic' n K ∧ degree P = degree (cyclotomic' n K) ∧ Monic P
refine' lifts_and_degree_eq_and_monic _ (cyclotomic'.monic n K)
case h
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
ihk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
⊢ cyclotomic' k K ∈ lifts (Int.castRingHom K)
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ cyclotomic' n K ∈ lifts (Int.castRingHom K)
induction' n using Nat.strong_induction_on with k ihk generalizing ζ
case h.inl
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
ζ : K
ihk : ∀ (m : ℕ), m < 0 → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
h : IsPrimitiveRoot ζ 0
⊢ cyclotomic' 0 K ∈ lifts (Int.castRingHom K)

case h.inr
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
ihk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
⊢ cyclotomic' k K ∈ lifts (Int.castRingHom K)
case h
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
ihk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
⊢ cyclotomic' k K ∈ lifts (Int.castRingHom K)
rcases k.eq_zero_or_pos with (rfl | hpos)
case h.inr
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
ihk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i in Nat.properDivisors k, cyclotomic' i K
⊢ cyclotomic' k K ∈ lifts (Int.castRingHom K)
case h.inr
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
ihk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
⊢ cyclotomic' k K ∈ lifts (Int.castRingHom K)
let B : K[X] := ∏ i in Nat.properDivisors k, cyclotomic' i K
case h.inr
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
ihk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i in Nat.properDivisors k, cyclotomic' i K
Bmo : Monic B
⊢ cyclotomic' k K ∈ lifts (Int.castRingHom K)
case h.inr
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
ihk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i in Nat.properDivisors k, cyclotomic' i K
⊢ cyclotomic' k K ∈ lifts (Int.castRingHom K)
have Bmo : B.Monic := by
  apply monic_prod_of_monic
  intro i _
  exact cyclotomic'.monic i K
case h.inr
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
ihk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i in Nat.properDivisors k, cyclotomic' i K
Bmo : Monic B
Bint : B ∈ lifts (Int.castRingHom K)
⊢ cyclotomic' k K ∈ lifts (Int.castRingHom K)
case h.inr
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
ihk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i in Nat.properDivisors k, cyclotomic' i K
Bmo : Monic B
⊢ cyclotomic' k K ∈ lifts (Int.castRingHom K)
have Bint : B ∈ lifts (Int.castRingHom K) := by
  refine' Subsemiring.prod_mem (lifts (Int.castRingHom K)) _
  intro x hx
  have xsmall := (Nat.mem_properDivisors.1 hx).2
  obtain ⟨d, hd⟩ := (Nat.mem_properDivisors.1 hx).1
  rw [mul_comm] at hd
  exact ihk x xsmall (h.pow hpos hd)
case h.inr
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
ihk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i in Nat.properDivisors k, cyclotomic' i K
Bmo : Monic B
Bint : ∃ q, map (Int.castRingHom K) q = B ∧ degree q = degree B ∧ Monic q
⊢ cyclotomic' k K ∈ lifts (Int.castRingHom K)
case h.inr
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
ihk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i in Nat.properDivisors k, cyclotomic' i K
Bmo : Monic B
Bint : B ∈ lifts (Int.castRingHom K)
⊢ cyclotomic' k K ∈ lifts (Int.castRingHom K)
replace Bint := lifts_and_degree_eq_and_monic Bint Bmo
case h.inr.intro.intro.intro
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
ihk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i in Nat.properDivisors k, cyclotomic' i K
Bmo : Monic B
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left✝ : degree B₁ = degree B
hB₁mo : Monic B₁
⊢ cyclotomic' k K ∈ lifts (Int.castRingHom K)
case h.inr
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
ihk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i in Nat.properDivisors k, cyclotomic' i K
Bmo : Monic B
Bint : ∃ q, map (Int.castRingHom K) q = B ∧ degree q = degree B ∧ Monic q
⊢ cyclotomic' k K ∈ lifts (Int.castRingHom K)
obtain ⟨B₁, hB₁, _, hB₁mo⟩ := Bint
case h.inr.intro.intro.intro
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
ihk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i in Nat.properDivisors k, cyclotomic' i K
Bmo : Monic B
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left✝ : degree B₁ = degree B
hB₁mo : Monic B₁
Q₁ : ℤ[X] := (X ^ k - 1) /ₘ B₁
⊢ cyclotomic' k K ∈ lifts (Int.castRingHom K)
case h.inr.intro.intro.intro
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
ihk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i in Nat.properDivisors k, cyclotomic' i K
Bmo : Monic B
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left✝ : degree B₁ = degree B
hB₁mo : Monic B₁
⊢ cyclotomic' k K ∈ lifts (Int.castRingHom K)
let Q₁ : ℤ[X] := (X ^ k - 1) /ₘ B₁
case h.inr.intro.intro.intro
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
ihk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i in Nat.properDivisors k, cyclotomic' i K
Bmo : Monic B
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left✝ : degree B₁ = degree B
hB₁mo : Monic B₁
Q₁ : ℤ[X] := (X ^ k - 1) /ₘ B₁
huniq : (X ^ k - 1) /ₘ B = cyclotomic' k K ∧ (X ^ k - 1) %ₘ B = 0
⊢ cyclotomic' k K ∈ lifts (Int.castRingHom K)
case h.inr.intro.intro.intro
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
ihk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i in Nat.properDivisors k, cyclotomic' i K
Bmo : Monic B
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left✝ : degree B₁ = degree B
hB₁mo : Monic B₁
Q₁ : ℤ[X] := (X ^ k - 1) /ₘ B₁
huniq : 0 + B * cyclotomic' k K = X ^ k - 1 ∧ degree 0 < degree B
⊢ cyclotomic' k K ∈ lifts (Int.castRingHom K)
replace huniq := div_modByMonic_unique (cyclotomic' k K) (0 : K[X]) Bmo huniq
case h.inr.intro.intro.intro
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
ihk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i in Nat.properDivisors k, cyclotomic' i K
Bmo : Monic B
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left✝ : degree B₁ = degree B
hB₁mo : Monic B₁
Q₁ : ℤ[X] := (X ^ k - 1) /ₘ B₁
huniq : (X ^ k - 1) /ₘ B = cyclotomic' k K ∧ (X ^ k - 1) %ₘ B = 0
⊢ ∃ x, ↑(mapRingHom (Int.castRingHom K)) x = cyclotomic' k K
case h.inr.intro.intro.intro
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
ihk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i in Nat.properDivisors k, cyclotomic' i K
Bmo : Monic B
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left✝ : degree B₁ = degree B
hB₁mo : Monic B₁
Q₁ : ℤ[X] := (X ^ k - 1) /ₘ B₁
huniq : (X ^ k - 1) /ₘ B = cyclotomic' k K ∧ (X ^ k - 1) %ₘ B = 0
⊢ cyclotomic' k K ∈ lifts (Int.castRingHom K)
simp only [lifts, RingHom.mem_rangeS]
case h.inr.intro.intro.intro
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
ihk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i in Nat.properDivisors k, cyclotomic' i K
Bmo : Monic B
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left✝ : degree B₁ = degree B
hB₁mo : Monic B₁
Q₁ : ℤ[X] := (X ^ k - 1) /ₘ B₁
huniq : (X ^ k - 1) /ₘ B = cyclotomic' k K ∧ (X ^ k - 1) %ₘ B = 0
⊢ ↑(mapRingHom (Int.castRingHom K)) Q₁ = cyclotomic' k K
case h.inr.intro.intro.intro
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
ihk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i in Nat.properDivisors k, cyclotomic' i K
Bmo : Monic B
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left✝ : degree B₁ = degree B
hB₁mo : Monic B₁
Q₁ : ℤ[X] := (X ^ k - 1) /ₘ B₁
huniq : (X ^ k - 1) /ₘ B = cyclotomic' k K ∧ (X ^ k - 1) %ₘ B = 0
⊢ ∃ x, ↑(mapRingHom (Int.castRingHom K)) x = cyclotomic' k K
use Q₁
case h.inr.intro.intro.intro
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
ihk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i in Nat.properDivisors k, cyclotomic' i K
Bmo : Monic B
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left✝ : degree B₁ = degree B
hB₁mo : Monic B₁
Q₁ : ℤ[X] := (X ^ k - 1) /ₘ B₁
huniq : (X ^ k - 1) /ₘ B = cyclotomic' k K ∧ (X ^ k - 1) %ₘ B = 0
⊢ map (Int.castRingHom K) (X ^ k - 1) /ₘ B = (X ^ k - 1) /ₘ B
case h.inr.intro.intro.intro
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
ihk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i in Nat.properDivisors k, cyclotomic' i K
Bmo : Monic B
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left✝ : degree B₁ = degree B
hB₁mo : Monic B₁
Q₁ : ℤ[X] := (X ^ k - 1) /ₘ B₁
huniq : (X ^ k - 1) /ₘ B = cyclotomic' k K ∧ (X ^ k - 1) %ₘ B = 0
⊢ ↑(mapRingHom (Int.castRingHom K)) Q₁ = cyclotomic' k K
rw [coe_mapRingHom, map_divByMonic (Int.castRingHom K) hB₁mo, hB₁, ← huniq.1]
no goals
case h.inr.intro.intro.intro
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
ihk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i in Nat.properDivisors k, cyclotomic' i K
Bmo : Monic B
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left✝ : degree B₁ = degree B
hB₁mo : Monic B₁
Q₁ : ℤ[X] := (X ^ k - 1) /ₘ B₁
huniq : (X ^ k - 1) /ₘ B = cyclotomic' k K ∧ (X ^ k - 1) %ₘ B = 0
⊢ map (Int.castRingHom K) (X ^ k - 1) /ₘ B = (X ^ k - 1) /ₘ B
simp
case h.inl
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
ζ : K
ihk : ∀ (m : ℕ), m < 0 → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
h : IsPrimitiveRoot ζ 0
⊢ ↑(mapRingHom (Int.castRingHom K)) 1 = cyclotomic' 0 K
case h.inl
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
ζ : K
ihk : ∀ (m : ℕ), m < 0 → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
h : IsPrimitiveRoot ζ 0
⊢ cyclotomic' 0 K ∈ lifts (Int.castRingHom K)
use 1
no goals
case h.inl
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
ζ : K
ihk : ∀ (m : ℕ), m < 0 → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
h : IsPrimitiveRoot ζ 0
⊢ ↑(mapRingHom (Int.castRingHom K)) 1 = cyclotomic' 0 K
simp only [cyclotomic'_zero, coe_mapRingHom, Polynomial.map_one]
case hs
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
ihk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i in Nat.properDivisors k, cyclotomic' i K
⊢ ∀ (i : ℕ), i ∈ Nat.properDivisors k → Monic (cyclotomic' i K)
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
ihk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i in Nat.properDivisors k, cyclotomic' i K
⊢ Monic B
apply monic_prod_of_monic
case hs
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
ihk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i in Nat.properDivisors k, cyclotomic' i K
i : ℕ
a✝ : i ∈ Nat.properDivisors k
⊢ Monic (cyclotomic' i K)
case hs
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
ihk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i in Nat.properDivisors k, cyclotomic' i K
⊢ ∀ (i : ℕ), i ∈ Nat.properDivisors k → Monic (cyclotomic' i K)
intro i _
no goals
case hs
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
ihk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i in Nat.properDivisors k, cyclotomic' i K
i : ℕ
a✝ : i ∈ Nat.properDivisors k
⊢ Monic (cyclotomic' i K)
exact cyclotomic'.monic i K
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
ihk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i in Nat.properDivisors k, cyclotomic' i K
Bmo : Monic B
⊢ ∀ (c : ℕ), c ∈ Nat.properDivisors k → cyclotomic' c K ∈ lifts (Int.castRingHom K)
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
ihk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i in Nat.properDivisors k, cyclotomic' i K
Bmo : Monic B
⊢ B ∈ lifts (Int.castRingHom K)
refine' Subsemiring.prod_mem (lifts (Int.castRingHom K)) _
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
ihk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i in Nat.properDivisors k, cyclotomic' i K
Bmo : Monic B
x : ℕ
hx : x ∈ Nat.properDivisors k
⊢ cyclotomic' x K ∈ lifts (Int.castRingHom K)
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
ihk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i in Nat.properDivisors k, cyclotomic' i K
Bmo : Monic B
⊢ ∀ (c : ℕ), c ∈ Nat.properDivisors k → cyclotomic' c K ∈ lifts (Int.castRingHom K)
intro x hx
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
ihk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i in Nat.properDivisors k, cyclotomic' i K
Bmo : Monic B
x : ℕ
hx : x ∈ Nat.properDivisors k
xsmall : x < k
⊢ cyclotomic' x K ∈ lifts (Int.castRingHom K)
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
ihk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i in Nat.properDivisors k, cyclotomic' i K
Bmo : Monic B
x : ℕ
hx : x ∈ Nat.properDivisors k
⊢ cyclotomic' x K ∈ lifts (Int.castRingHom K)
have xsmall := (Nat.mem_properDivisors.1 hx).2
case intro
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
ihk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i in Nat.properDivisors k, cyclotomic' i K
Bmo : Monic B
x : ℕ
hx : x ∈ Nat.properDivisors k
xsmall : x < k
d : ℕ
hd : k = x * d
⊢ cyclotomic' x K ∈ lifts (Int.castRingHom K)
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
ihk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i in Nat.properDivisors k, cyclotomic' i K
Bmo : Monic B
x : ℕ
hx : x ∈ Nat.properDivisors k
xsmall : x < k
⊢ cyclotomic' x K ∈ lifts (Int.castRingHom K)
obtain ⟨d, hd⟩ := (Nat.mem_properDivisors.1 hx).1
case intro
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
ihk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i in Nat.properDivisors k, cyclotomic' i K
Bmo : Monic B
x : ℕ
hx : x ∈ Nat.properDivisors k
xsmall : x < k
d : ℕ
hd : k = d * x
⊢ cyclotomic' x K ∈ lifts (Int.castRingHom K)
case intro
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
ihk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i in Nat.properDivisors k, cyclotomic' i K
Bmo : Monic B
x : ℕ
hx : x ∈ Nat.properDivisors k
xsmall : x < k
d : ℕ
hd : k = x * d
⊢ cyclotomic' x K ∈ lifts (Int.castRingHom K)
rw [mul_comm] at hd
no goals
case intro
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
ihk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i in Nat.properDivisors k, cyclotomic' i K
Bmo : Monic B
x : ℕ
hx : x ∈ Nat.properDivisors k
xsmall : x < k
d : ℕ
hd : k = d * x
⊢ cyclotomic' x K ∈ lifts (Int.castRingHom K)
exact ihk x xsmall (h.pow hpos hd)
case left
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
ihk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i in Nat.properDivisors k, cyclotomic' i K
Bmo : Monic B
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left✝ : degree B₁ = degree B
hB₁mo : Monic B₁
Q₁ : ℤ[X] := (X ^ k - 1) /ₘ B₁
⊢ 0 + B * cyclotomic' k K = X ^ k - 1

case right
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
ihk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i in Nat.properDivisors k, cyclotomic' i K
Bmo : Monic B
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left✝ : degree B₁ = degree B
hB₁mo : Monic B₁
Q₁ : ℤ[X] := (X ^ k - 1) /ₘ B₁
⊢ degree 0 < degree B
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
ihk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i in Nat.properDivisors k, cyclotomic' i K
Bmo : Monic B
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left✝ : degree B₁ = degree B
hB₁mo : Monic B₁
Q₁ : ℤ[X] := (X ^ k - 1) /ₘ B₁
⊢ 0 + B * cyclotomic' k K = X ^ k - 1 ∧ degree 0 < degree B
constructor
no goals
case left
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
ihk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i in Nat.properDivisors k, cyclotomic' i K
Bmo : Monic B
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left✝ : degree B₁ = degree B
hB₁mo : Monic B₁
Q₁ : ℤ[X] := (X ^ k - 1) /ₘ B₁
⊢ 0 + B * cyclotomic' k K = X ^ k - 1
rw [zero_add, mul_comm, ← prod_cyclotomic'_eq_X_pow_sub_one hpos h, ←
  Nat.cons_self_properDivisors hpos.ne', Finset.prod_cons]
no goals
case right
K✝ : Type ?u.247792
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
h✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
ihk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i in Nat.properDivisors k, cyclotomic' i K
Bmo : Monic B
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left✝ : degree B₁ = degree B
hB₁mo : Monic B₁
Q₁ : ℤ[X] := (X ^ k - 1) /ₘ B₁
⊢ degree 0 < degree B
simpa only [degree_zero, bot_lt_iff_ne_bot, Ne.def, degree_eq_bot] using Bmo.ne_zero