[GOAL]
R✝ : Type u_1
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ cyclotomic' 0 R = 1
[PROOFSTEP]
simp only [cyclotomic', Finset.prod_empty, primitiveRoots_zero]
[GOAL]
R✝ : Type u_1
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ cyclotomic' 1 R = X - 1
[PROOFSTEP]
simp only [cyclotomic', Finset.prod_singleton, RingHom.map_one, IsPrimitiveRoot.primitiveRoots_one]
[GOAL]
R✝ : Type u_1
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : ℕ
inst✝ : CharP R p
hp : p ≠ 2
⊢ cyclotomic' 2 R = X + 1
[PROOFSTEP]
rw [cyclotomic']
[GOAL]
R✝ : Type u_1
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : ℕ
inst✝ : CharP R p
hp : p ≠ 2
⊢ ∏ μ in primitiveRoots 2 R, (X - ↑C μ) = X + 1
[PROOFSTEP]
have prim_root_two : primitiveRoots 2 R = {(-1 : R)} :=
  by
  simp only [Finset.eq_singleton_iff_unique_mem, mem_primitiveRoots two_pos]
  exact ⟨IsPrimitiveRoot.neg_one p hp, fun x => IsPrimitiveRoot.eq_neg_one_of_two_right⟩
[GOAL]
R✝ : Type u_1
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : ℕ
inst✝ : CharP R p
hp : p ≠ 2
⊢ primitiveRoots 2 R = {-1}
[PROOFSTEP]
simp only [Finset.eq_singleton_iff_unique_mem, mem_primitiveRoots two_pos]
[GOAL]
R✝ : Type u_1
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : ℕ
inst✝ : CharP R p
hp : p ≠ 2
⊢ IsPrimitiveRoot (-1) 2 ∧ ∀ (x : R), IsPrimitiveRoot x 2 → x = -1
[PROOFSTEP]
exact ⟨IsPrimitiveRoot.neg_one p hp, fun x => IsPrimitiveRoot.eq_neg_one_of_two_right⟩
[GOAL]
R✝ : Type u_1
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : ℕ
inst✝ : CharP R p
hp : p ≠ 2
prim_root_two : primitiveRoots 2 R = {-1}
⊢ ∏ μ in primitiveRoots 2 R, (X - ↑C μ) = X + 1
[PROOFSTEP]
simp only [prim_root_two, Finset.prod_singleton, RingHom.map_neg, RingHom.map_one, sub_neg_eq_add]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ natDegree (cyclotomic' n R) = Nat.totient n
[PROOFSTEP]
rw [cyclotomic']
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ natDegree (∏ μ in primitiveRoots n R, (X - ↑C μ)) = Nat.totient n
[PROOFSTEP]
rw [natDegree_prod (primitiveRoots n R) fun z : R => X - C z]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ ∑ i in primitiveRoots n R, natDegree (X - ↑C i) = Nat.totient n
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ ∀ (i : R), i ∈ primitiveRoots n R → X - ↑C i ≠ 0
[PROOFSTEP]
simp only [IsPrimitiveRoot.card_primitiveRoots h, mul_one, natDegree_X_sub_C, Nat.cast_id, Finset.sum_const,
  nsmul_eq_mul]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ ∀ (i : R), i ∈ primitiveRoots n R → X - ↑C i ≠ 0
[PROOFSTEP]
intro z _
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
z : R
a✝ : z ∈ primitiveRoots n R
⊢ X - ↑C z ≠ 0
[PROOFSTEP]
exact X_sub_C_ne_zero z
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ degree (cyclotomic' n R) = ↑(Nat.totient n)
[PROOFSTEP]
simp only [degree_eq_natDegree (cyclotomic'_ne_zero n R), natDegree_cyclotomic' h]
[GOAL]
R✝ : Type u_1
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
n : ℕ
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ roots (cyclotomic' n R) = (primitiveRoots n R).val
[PROOFSTEP]
rw [cyclotomic']
[GOAL]
R✝ : Type u_1
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
n : ℕ
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ roots (∏ μ in primitiveRoots n R, (X - ↑C μ)) = (primitiveRoots n R).val
[PROOFSTEP]
exact roots_prod_X_sub_C (primitiveRoots n R)
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ X ^ n - 1 = ∏ ζ in nthRootsFinset n R, (X - ↑C ζ)
[PROOFSTEP]
rw [nthRootsFinset, ← Multiset.toFinset_eq (IsPrimitiveRoot.nthRoots_nodup h)]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ X ^ n - 1 = ∏ ζ in { val := nthRoots n 1, nodup := (_ : Multiset.Nodup (nthRoots n 1)) }, (X - ↑C ζ)
[PROOFSTEP]
simp only [Finset.prod_mk, RingHom.map_one]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ X ^ n - 1 = Multiset.prod (Multiset.map (fun x => X - ↑C x) (nthRoots n 1))
[PROOFSTEP]
rw [nthRoots]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ X ^ n - 1 = Multiset.prod (Multiset.map (fun x => X - ↑C x) (roots (X ^ n - ↑C 1)))
[PROOFSTEP]
have hmonic : (X ^ n - C (1 : R)).Monic := monic_X_pow_sub_C (1 : R) (ne_of_lt hpos).symm
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hmonic : Monic (X ^ n - ↑C 1)
⊢ X ^ n - 1 = Multiset.prod (Multiset.map (fun x => X - ↑C x) (roots (X ^ n - ↑C 1)))
[PROOFSTEP]
symm
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hmonic : Monic (X ^ n - ↑C 1)
⊢ Multiset.prod (Multiset.map (fun x => X - ↑C x) (roots (X ^ n - ↑C 1))) = X ^ n - 1
[PROOFSTEP]
apply prod_multiset_X_sub_C_of_monic_of_roots_card_eq hmonic
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hmonic : Monic (X ^ n - ↑C 1)
⊢ ↑Multiset.card (roots (X ^ n - ↑C 1)) = natDegree (X ^ n - ↑C 1)
[PROOFSTEP]
rw [@natDegree_X_pow_sub_C R _ _ n 1, ← nthRoots]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hmonic : Monic (X ^ n - ↑C 1)
⊢ ↑Multiset.card (nthRoots n 1) = n
[PROOFSTEP]
exact IsPrimitiveRoot.card_nthRoots h
[GOAL]
K : Type u_1
inst✝ : Field K
n : ℕ
⊢ Splits (RingHom.id K) (cyclotomic' n K)
[PROOFSTEP]
apply splits_prod (RingHom.id K)
[GOAL]
K : Type u_1
inst✝ : Field K
n : ℕ
⊢ ∀ (j : K), j ∈ primitiveRoots n K → Splits (RingHom.id K) (X - ↑C j)
[PROOFSTEP]
intro z _
[GOAL]
K : Type u_1
inst✝ : Field K
n : ℕ
z : K
a✝ : z ∈ primitiveRoots n K
⊢ Splits (RingHom.id K) (X - ↑C z)
[PROOFSTEP]
simp only [splits_X_sub_C (RingHom.id K)]
[GOAL]
K : Type u_1
inst✝ : Field K
ζ : K
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ Splits (RingHom.id K) (X ^ n - ↑C 1)
[PROOFSTEP]
rw [splits_iff_card_roots, ← nthRoots, IsPrimitiveRoot.card_nthRoots h, natDegree_X_pow_sub_C]
[GOAL]
K✝ : Type u_1
inst✝² : Field K✝
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ ∏ i in Nat.divisors n, cyclotomic' i K = X ^ n - 1
[PROOFSTEP]
have hd : (n.divisors : Set ℕ).PairwiseDisjoint fun k => primitiveRoots k K := fun x _ y _ hne =>
  IsPrimitiveRoot.disjoint hne
[GOAL]
K✝ : Type u_1
inst✝² : Field K✝
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hd : Set.PairwiseDisjoint ↑(Nat.divisors n) fun k => primitiveRoots k K
⊢ ∏ i in Nat.divisors n, cyclotomic' i K = X ^ n - 1
[PROOFSTEP]
simp only [X_pow_sub_one_eq_prod hpos h, cyclotomic', ← Finset.prod_biUnion hd,
  h.nthRoots_one_eq_biUnion_primitiveRoots]
[GOAL]
K✝ : Type u_1
inst✝² : Field K✝
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ cyclotomic' n K = (X ^ n - 1) /ₘ ∏ i in Nat.properDivisors n, cyclotomic' i K
[PROOFSTEP]
rw [← prod_cyclotomic'_eq_X_pow_sub_one hpos h, ← Nat.cons_self_properDivisors hpos.ne', Finset.prod_cons]
[GOAL]
K✝ : Type u_1
inst✝² : Field K✝
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ cyclotomic' n K =
    (cyclotomic' n K * ∏ x in Nat.properDivisors n, cyclotomic' x K) /ₘ ∏ i in Nat.properDivisors n, cyclotomic' i K
[PROOFSTEP]
have prod_monic : (∏ i in Nat.properDivisors n, cyclotomic' i K).Monic :=
  by
  apply monic_prod_of_monic
  intro i _
  exact cyclotomic'.monic i K
[GOAL]
K✝ : Type u_1
inst✝² : Field K✝
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ Monic (∏ i in Nat.properDivisors n, cyclotomic' i K)
[PROOFSTEP]
apply monic_prod_of_monic
[GOAL]
case hs
K✝ : Type u_1
inst✝² : Field K✝
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ ∀ (i : ℕ), i ∈ Nat.properDivisors n → Monic (cyclotomic' i K)
[PROOFSTEP]
intro i _
[GOAL]
case hs
K✝ : Type u_1
inst✝² : Field K✝
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
i : ℕ
a✝ : i ∈ Nat.properDivisors n
⊢ Monic (cyclotomic' i K)
[PROOFSTEP]
exact cyclotomic'.monic i K
[GOAL]
K✝ : Type u_1
inst✝² : Field K✝
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
prod_monic : Monic (∏ i in Nat.properDivisors n, cyclotomic' i K)
⊢ cyclotomic' n K =
    (cyclotomic' n K * ∏ x in Nat.properDivisors n, cyclotomic' x K) /ₘ ∏ i in Nat.properDivisors n, cyclotomic' i K
[PROOFSTEP]
rw [(div_modByMonic_unique (cyclotomic' n K) 0 prod_monic _).1]
[GOAL]
K✝ : Type u_1
inst✝² : Field K✝
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
prod_monic : Monic (∏ i in Nat.properDivisors n, cyclotomic' i K)
⊢ 0 + (∏ i in Nat.properDivisors n, cyclotomic' i K) * cyclotomic' n K =
      cyclotomic' n K * ∏ x in Nat.properDivisors n, cyclotomic' x K ∧
    degree 0 < degree (∏ i in Nat.properDivisors n, cyclotomic' i K)
[PROOFSTEP]
simp only [degree_zero, zero_add]
[GOAL]
K✝ : Type u_1
inst✝² : Field K✝
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
prod_monic : Monic (∏ i in Nat.properDivisors n, cyclotomic' i K)
⊢ (∏ i in Nat.properDivisors n, cyclotomic' i K) * cyclotomic' n K =
      cyclotomic' n K * ∏ i in Nat.properDivisors n, cyclotomic' i K ∧
    ⊥ < degree (∏ i in Nat.properDivisors n, cyclotomic' i K)
[PROOFSTEP]
refine' ⟨by rw [mul_comm], _⟩
[GOAL]
K✝ : Type u_1
inst✝² : Field K✝
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
prod_monic : Monic (∏ i in Nat.properDivisors n, cyclotomic' i K)
⊢ (∏ i in Nat.properDivisors n, cyclotomic' i K) * cyclotomic' n K =
    cyclotomic' n K * ∏ i in Nat.properDivisors n, cyclotomic' i K
[PROOFSTEP]
rw [mul_comm]
[GOAL]
K✝ : Type u_1
inst✝² : Field K✝
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
prod_monic : Monic (∏ i in Nat.properDivisors n, cyclotomic' i K)
⊢ ⊥ < degree (∏ i in Nat.properDivisors n, cyclotomic' i K)
[PROOFSTEP]
rw [bot_lt_iff_ne_bot]
[GOAL]
K✝ : Type u_1
inst✝² : Field K✝
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
prod_monic : Monic (∏ i in Nat.properDivisors n, cyclotomic' i K)
⊢ degree (∏ i in Nat.properDivisors n, cyclotomic' i K) ≠ ⊥
[PROOFSTEP]
intro h
[GOAL]
K✝ : Type u_1
inst✝² : Field K✝
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h✝ : IsPrimitiveRoot ζ n
prod_monic : Monic (∏ i in Nat.properDivisors n, cyclotomic' i K)
h : degree (∏ i in Nat.properDivisors n, cyclotomic' i K) = ⊥
⊢ False
[PROOFSTEP]
exact Monic.ne_zero prod_monic (degree_eq_bot.1 h)
[GOAL]
K✝ : Type u_1
inst✝² : Field K✝
K : Type u_2
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
[PROOFSTEP]
refine' lifts_and_degree_eq_and_monic _ (cyclotomic'.monic n K)
[GOAL]
K✝ : Type u_1
inst✝² : Field K✝
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ cyclotomic' n K ∈ lifts (Int.castRingHom K)
[PROOFSTEP]
induction' n using Nat.strong_induction_on with k ihk generalizing ζ
[GOAL]
case h
K✝ : Type u_1
inst✝² : Field K✝
K : Type u_2
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)
[PROOFSTEP]
rcases k.eq_zero_or_pos with (rfl | hpos)
[GOAL]
case h.inl
K✝ : Type u_1
inst✝² : Field K✝
K : Type u_2
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)
[PROOFSTEP]
use 1
[GOAL]
case h
K✝ : Type u_1
inst✝² : Field K✝
K : Type u_2
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
[PROOFSTEP]
simp only [cyclotomic'_zero, coe_mapRingHom, Polynomial.map_one]
[GOAL]
case h.inr
K✝ : Type u_1
inst✝² : Field K✝
K : Type u_2
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)
[PROOFSTEP]
let B : K[X] := ∏ i in Nat.properDivisors k, cyclotomic' i K
[GOAL]
case h.inr
K✝ : Type u_1
inst✝² : Field K✝
K : Type u_2
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)
[PROOFSTEP]
have Bmo : B.Monic := by
  apply monic_prod_of_monic
  intro i _
  exact cyclotomic'.monic i K
[GOAL]
K✝ : Type u_1
inst✝² : Field K✝
K : Type u_2
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
[PROOFSTEP]
apply monic_prod_of_monic
[GOAL]
case hs
K✝ : Type u_1
inst✝² : Field K✝
K : Type u_2
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)
[PROOFSTEP]
intro i _
[GOAL]
case hs
K✝ : Type u_1
inst✝² : Field K✝
K : Type u_2
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)
[PROOFSTEP]
exact cyclotomic'.monic i K
[GOAL]
case h.inr
K✝ : Type u_1
inst✝² : Field K✝
K : Type u_2
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)
[PROOFSTEP]
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)
[GOAL]
K✝ : Type u_1
inst✝² : Field K✝
K : Type u_2
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)
[PROOFSTEP]
refine' Subsemiring.prod_mem (lifts (Int.castRingHom K)) _
[GOAL]
K✝ : Type u_1
inst✝² : Field K✝
K : Type u_2
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)
[PROOFSTEP]
intro x hx
[GOAL]
K✝ : Type u_1
inst✝² : Field K✝
K : Type u_2
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)
[PROOFSTEP]
have xsmall := (Nat.mem_properDivisors.1 hx).2
[GOAL]
K✝ : Type u_1
inst✝² : Field K✝
K : Type u_2
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)
[PROOFSTEP]
obtain ⟨d, hd⟩ := (Nat.mem_properDivisors.1 hx).1
[GOAL]
case intro
K✝ : Type u_1
inst✝² : Field K✝
K : Type u_2
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)
[PROOFSTEP]
rw [mul_comm] at hd
[GOAL]
case intro
K✝ : Type u_1
inst✝² : Field K✝
K : Type u_2
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)
[PROOFSTEP]
exact ihk x xsmall (h.pow hpos hd)
[GOAL]
case h.inr
K✝ : Type u_1
inst✝² : Field K✝
K : Type u_2
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)
[PROOFSTEP]
replace Bint := lifts_and_degree_eq_and_monic Bint Bmo
[GOAL]
case h.inr
K✝ : Type u_1
inst✝² : Field K✝
K : Type u_2
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)
[PROOFSTEP]
obtain ⟨B₁, hB₁, _, hB₁mo⟩ := Bint
[GOAL]
case h.inr.intro.intro.intro
K✝ : Type u_1
inst✝² : Field K✝
K : Type u_2
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)
[PROOFSTEP]
let Q₁ : ℤ[X] := (X ^ k - 1) /ₘ B₁
[GOAL]
case h.inr.intro.intro.intro
K✝ : Type u_1
inst✝² : Field K✝
K : Type u_2
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)
[PROOFSTEP]
have huniq : 0 + B * cyclotomic' k K = X ^ k - 1 ∧ (0 : K[X]).degree < B.degree :=
  by
  constructor
  ·
    rw [zero_add, mul_comm, ← prod_cyclotomic'_eq_X_pow_sub_one hpos h, ← Nat.cons_self_properDivisors hpos.ne',
      Finset.prod_cons]
  · simpa only [degree_zero, bot_lt_iff_ne_bot, Ne.def, degree_eq_bot] using Bmo.ne_zero
[GOAL]
K✝ : Type u_1
inst✝² : Field K✝
K : Type u_2
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
[PROOFSTEP]
constructor
[GOAL]
case left
K✝ : Type u_1
inst✝² : Field K✝
K : Type u_2
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
[PROOFSTEP]
rw [zero_add, mul_comm, ← prod_cyclotomic'_eq_X_pow_sub_one hpos h, ← Nat.cons_self_properDivisors hpos.ne',
  Finset.prod_cons]
[GOAL]
case right
K✝ : Type u_1
inst✝² : Field K✝
K : Type u_2
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
[PROOFSTEP]
simpa only [degree_zero, bot_lt_iff_ne_bot, Ne.def, degree_eq_bot] using Bmo.ne_zero
[GOAL]
case h.inr.intro.intro.intro
K✝ : Type u_1
inst✝² : Field K✝
K : Type u_2
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)
[PROOFSTEP]
replace huniq := div_modByMonic_unique (cyclotomic' k K) (0 : K[X]) Bmo huniq
[GOAL]
case h.inr.intro.intro.intro
K✝ : Type u_1
inst✝² : Field K✝
K : Type u_2
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)
[PROOFSTEP]
simp only [lifts, RingHom.mem_rangeS]
[GOAL]
case h.inr.intro.intro.intro
K✝ : Type u_1
inst✝² : Field K✝
K : Type u_2
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
[PROOFSTEP]
use Q₁
[GOAL]
case h
K✝ : Type u_1
inst✝² : Field K✝
K : Type u_2
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
[PROOFSTEP]
rw [coe_mapRingHom, map_divByMonic (Int.castRingHom K) hB₁mo, hB₁, ← huniq.1]
[GOAL]
case h
K✝ : Type u_1
inst✝² : Field K✝
K : Type u_2
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
[PROOFSTEP]
simp
[GOAL]
K✝ : Type u_1
inst✝³ : Field K✝
K : Type u_2
inst✝² : CommRing K
inst✝¹ : IsDomain K
inst✝ : CharZero K
ζ : K
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
⊢ ∃! P, map (Int.castRingHom K) P = cyclotomic' (↑n) K
[PROOFSTEP]
obtain ⟨P, hP⟩ := int_coeff_of_cyclotomic' h
[GOAL]
case intro
K✝ : Type u_1
inst✝³ : Field K✝
K : Type u_2
inst✝² : CommRing K
inst✝¹ : IsDomain K
inst✝ : CharZero K
ζ : K
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
P : ℤ[X]
hP : map (Int.castRingHom K) P = cyclotomic' (↑n) K ∧ degree P = degree (cyclotomic' (↑n) K) ∧ Monic P
⊢ ∃! P, map (Int.castRingHom K) P = cyclotomic' (↑n) K
[PROOFSTEP]
refine' ⟨P, hP.1, fun Q hQ => _⟩
[GOAL]
case intro
K✝ : Type u_1
inst✝³ : Field K✝
K : Type u_2
inst✝² : CommRing K
inst✝¹ : IsDomain K
inst✝ : CharZero K
ζ : K
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
P : ℤ[X]
hP : map (Int.castRingHom K) P = cyclotomic' (↑n) K ∧ degree P = degree (cyclotomic' (↑n) K) ∧ Monic P
Q : ℤ[X]
hQ : (fun P => map (Int.castRingHom K) P = cyclotomic' (↑n) K) Q
⊢ Q = P
[PROOFSTEP]
apply map_injective (Int.castRingHom K) Int.cast_injective
[GOAL]
case intro.a
K✝ : Type u_1
inst✝³ : Field K✝
K : Type u_2
inst✝² : CommRing K
inst✝¹ : IsDomain K
inst✝ : CharZero K
ζ : K
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
P : ℤ[X]
hP : map (Int.castRingHom K) P = cyclotomic' (↑n) K ∧ degree P = degree (cyclotomic' (↑n) K) ∧ Monic P
Q : ℤ[X]
hQ : (fun P => map (Int.castRingHom K) P = cyclotomic' (↑n) K) Q
⊢ map (Int.castRingHom K) Q = map (Int.castRingHom K) P
[PROOFSTEP]
rw [hP.1, hQ]
[GOAL]
n : ℕ
h : n ≠ 0
⊢ cyclotomic n ℤ =
    Exists.choose (_ : ∃ P, map (Int.castRingHom ℂ) P = cyclotomic' n ℂ ∧ degree P = degree (cyclotomic' n ℂ) ∧ Monic P)
[PROOFSTEP]
simp only [cyclotomic, h, dif_neg, not_false_iff]
[GOAL]
n : ℕ
h : n ≠ 0
⊢ map (Int.castRingHom ℤ)
      (Exists.choose
        (_ : ∃ P, map (Int.castRingHom ℂ) P = cyclotomic' n ℂ ∧ degree P = degree (cyclotomic' n ℂ) ∧ Monic P)) =
    Exists.choose (_ : ∃ P, map (Int.castRingHom ℂ) P = cyclotomic' n ℂ ∧ degree P = degree (cyclotomic' n ℂ) ∧ Monic P)
[PROOFSTEP]
ext i
[GOAL]
case a
n : ℕ
h : n ≠ 0
i : ℕ
⊢ coeff
      (map (Int.castRingHom ℤ)
        (Exists.choose
          (_ : ∃ P, map (Int.castRingHom ℂ) P = cyclotomic' n ℂ ∧ degree P = degree (cyclotomic' n ℂ) ∧ Monic P)))
      i =
    coeff
      (Exists.choose
        (_ : ∃ P, map (Int.castRingHom ℂ) P = cyclotomic' n ℂ ∧ degree P = degree (cyclotomic' n ℂ) ∧ Monic P))
      i
[PROOFSTEP]
simp only [coeff_map, Int.cast_id, eq_intCast]
[GOAL]
n : ℕ
R : Type u_1
inst✝ : Ring R
⊢ map (Int.castRingHom R) (cyclotomic n ℤ) = cyclotomic n R
[PROOFSTEP]
by_cases hzero : n = 0
[GOAL]
case pos
n : ℕ
R : Type u_1
inst✝ : Ring R
hzero : n = 0
⊢ map (Int.castRingHom R) (cyclotomic n ℤ) = cyclotomic n R
[PROOFSTEP]
simp only [hzero, cyclotomic, dif_pos, Polynomial.map_one]
[GOAL]
case neg
n : ℕ
R : Type u_1
inst✝ : Ring R
hzero : ¬n = 0
⊢ map (Int.castRingHom R) (cyclotomic n ℤ) = cyclotomic n R
[PROOFSTEP]
simp [cyclotomic, hzero]
[GOAL]
n : ℕ
⊢ map (Int.castRingHom ℂ) (cyclotomic n ℤ) = cyclotomic' n ℂ ∧
    degree (cyclotomic n ℤ) = degree (cyclotomic' n ℂ) ∧ Monic (cyclotomic n ℤ)
[PROOFSTEP]
by_cases hzero : n = 0
[GOAL]
case pos
n : ℕ
hzero : n = 0
⊢ map (Int.castRingHom ℂ) (cyclotomic n ℤ) = cyclotomic' n ℂ ∧
    degree (cyclotomic n ℤ) = degree (cyclotomic' n ℂ) ∧ Monic (cyclotomic n ℤ)
[PROOFSTEP]
simp only [hzero, cyclotomic, degree_one, monic_one, cyclotomic'_zero, dif_pos, eq_self_iff_true, Polynomial.map_one,
  and_self_iff]
[GOAL]
case neg
n : ℕ
hzero : ¬n = 0
⊢ map (Int.castRingHom ℂ) (cyclotomic n ℤ) = cyclotomic' n ℂ ∧
    degree (cyclotomic n ℤ) = degree (cyclotomic' n ℂ) ∧ Monic (cyclotomic n ℤ)
[PROOFSTEP]
rw [int_cyclotomic_rw hzero]
[GOAL]
case neg
n : ℕ
hzero : ¬n = 0
⊢ map (Int.castRingHom ℂ)
        (Exists.choose
          (_ : ∃ P, map (Int.castRingHom ℂ) P = cyclotomic' n ℂ ∧ degree P = degree (cyclotomic' n ℂ) ∧ Monic P)) =
      cyclotomic' n ℂ ∧
    degree
          (Exists.choose
            (_ : ∃ P, map (Int.castRingHom ℂ) P = cyclotomic' n ℂ ∧ degree P = degree (cyclotomic' n ℂ) ∧ Monic P)) =
        degree (cyclotomic' n ℂ) ∧
      Monic
        (Exists.choose
          (_ : ∃ P, map (Int.castRingHom ℂ) P = cyclotomic' n ℂ ∧ degree P = degree (cyclotomic' n ℂ) ∧ Monic P))
[PROOFSTEP]
exact (int_coeff_of_cyclotomic' (Complex.isPrimitiveRoot_exp n hzero)).choose_spec
[GOAL]
n : ℕ
P : ℤ[X]
h : map (Int.castRingHom ℂ) P = cyclotomic' n ℂ
⊢ P = cyclotomic n ℤ
[PROOFSTEP]
apply map_injective (Int.castRingHom ℂ) Int.cast_injective
[GOAL]
case a
n : ℕ
P : ℤ[X]
h : map (Int.castRingHom ℂ) P = cyclotomic' n ℂ
⊢ map (Int.castRingHom ℂ) P = map (Int.castRingHom ℂ) (cyclotomic n ℤ)
[PROOFSTEP]
rw [h, (int_cyclotomic_spec n).1]
[GOAL]
n : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
⊢ map f (cyclotomic n R) = cyclotomic n S
[PROOFSTEP]
rw [← map_cyclotomic_int n R, ← map_cyclotomic_int n S, map_map]
[GOAL]
n : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
⊢ map (RingHom.comp f (Int.castRingHom R)) (cyclotomic n ℤ) = map (Int.castRingHom S) (cyclotomic n ℤ)
[PROOFSTEP]
congr!
[GOAL]
R : Type u_1
S : Type u_2
q : R
n : ℕ
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
⊢ eval (↑f q) (cyclotomic n S) = ↑f (eval q (cyclotomic n R))
[PROOFSTEP]
rw [← map_cyclotomic n f, eval_map, eval₂_at_apply]
[GOAL]
R : Type u_1
inst✝ : Ring R
⊢ cyclotomic 0 R = 1
[PROOFSTEP]
simp only [cyclotomic, dif_pos]
[GOAL]
R : Type u_1
inst✝ : Ring R
⊢ cyclotomic 1 R = X - 1
[PROOFSTEP]
have hspec : map (Int.castRingHom ℂ) (X - 1) = cyclotomic' 1 ℂ := by
  simp only [cyclotomic'_one, PNat.one_coe, map_X, Polynomial.map_one, Polynomial.map_sub]
[GOAL]
R : Type u_1
inst✝ : Ring R
⊢ map (Int.castRingHom ℂ) (X - 1) = cyclotomic' 1 ℂ
[PROOFSTEP]
simp only [cyclotomic'_one, PNat.one_coe, map_X, Polynomial.map_one, Polynomial.map_sub]
[GOAL]
R : Type u_1
inst✝ : Ring R
hspec : map (Int.castRingHom ℂ) (X - 1) = cyclotomic' 1 ℂ
⊢ cyclotomic 1 R = X - 1
[PROOFSTEP]
symm
[GOAL]
R : Type u_1
inst✝ : Ring R
hspec : map (Int.castRingHom ℂ) (X - 1) = cyclotomic' 1 ℂ
⊢ X - 1 = cyclotomic 1 R
[PROOFSTEP]
rw [← map_cyclotomic_int, ← int_cyclotomic_unique hspec]
[GOAL]
R : Type u_1
inst✝ : Ring R
hspec : map (Int.castRingHom ℂ) (X - 1) = cyclotomic' 1 ℂ
⊢ X - 1 = map (Int.castRingHom R) (X - 1)
[PROOFSTEP]
simp only [map_X, Polynomial.map_one, Polynomial.map_sub]
[GOAL]
n : ℕ
R : Type u_1
inst✝ : Ring R
⊢ Monic (cyclotomic n R)
[PROOFSTEP]
rw [← map_cyclotomic_int]
[GOAL]
n : ℕ
R : Type u_1
inst✝ : Ring R
⊢ Monic (map (Int.castRingHom R) (cyclotomic n ℤ))
[PROOFSTEP]
exact (int_cyclotomic_spec n).2.2.map _
[GOAL]
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ degree (cyclotomic n R) = ↑(Nat.totient n)
[PROOFSTEP]
rw [← map_cyclotomic_int]
[GOAL]
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ degree (map (Int.castRingHom R) (cyclotomic n ℤ)) = ↑(Nat.totient n)
[PROOFSTEP]
rw [degree_map_eq_of_leadingCoeff_ne_zero (Int.castRingHom R) _]
[GOAL]
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ degree (cyclotomic n ℤ) = ↑(Nat.totient n)
[PROOFSTEP]
cases' n with k
[GOAL]
case zero
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ degree (cyclotomic Nat.zero ℤ) = ↑(Nat.totient Nat.zero)
[PROOFSTEP]
simp only [cyclotomic, degree_one, dif_pos, Nat.totient_zero, WithTop.coe_zero]
[GOAL]
case succ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
k : ℕ
⊢ degree (cyclotomic (Nat.succ k) ℤ) = ↑(Nat.totient (Nat.succ k))
[PROOFSTEP]
rw [← degree_cyclotomic' (Complex.isPrimitiveRoot_exp k.succ (Nat.succ_ne_zero k))]
[GOAL]
case succ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
k : ℕ
⊢ degree (cyclotomic (Nat.succ k) ℤ) = degree (cyclotomic' (Nat.succ k) ℂ)
[PROOFSTEP]
exact (int_cyclotomic_spec k.succ).2.1
[GOAL]
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ ↑(Int.castRingHom R) (leadingCoeff (cyclotomic n ℤ)) ≠ 0
[PROOFSTEP]
simp only [(int_cyclotomic_spec n).right.right, eq_intCast, Monic.leadingCoeff, Int.cast_one, Ne.def, not_false_iff,
  one_ne_zero]
[GOAL]
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ natDegree (cyclotomic n R) = Nat.totient n
[PROOFSTEP]
rw [natDegree, degree_cyclotomic]
[GOAL]
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ WithBot.unbot' 0 ↑(Nat.totient n) = Nat.totient n
[PROOFSTEP]
norm_cast
[GOAL]
n : ℕ
R : Type u_1
hpos : 0 < n
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ 0 < degree (cyclotomic n R)
[PROOFSTEP]
rw [degree_cyclotomic n R, Nat.cast_pos]
[GOAL]
n : ℕ
R : Type u_1
hpos : 0 < n
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ 0 < Nat.totient n
[PROOFSTEP]
exact Nat.totient_pos hpos
[GOAL]
n : ℕ
hpos : 0 < n
R : Type u_1
inst✝ : CommRing R
⊢ ∏ i in Nat.divisors n, cyclotomic i R = X ^ n - 1
[PROOFSTEP]
have integer : ∏ i in Nat.divisors n, cyclotomic i ℤ = X ^ n - 1 :=
  by
  apply map_injective (Int.castRingHom ℂ) Int.cast_injective
  simp only [Polynomial.map_prod, int_cyclotomic_spec, Polynomial.map_pow, map_X, Polynomial.map_one,
    Polynomial.map_sub]
  exact prod_cyclotomic'_eq_X_pow_sub_one hpos (Complex.isPrimitiveRoot_exp n hpos.ne')
[GOAL]
n : ℕ
hpos : 0 < n
R : Type u_1
inst✝ : CommRing R
⊢ ∏ i in Nat.divisors n, cyclotomic i ℤ = X ^ n - 1
[PROOFSTEP]
apply map_injective (Int.castRingHom ℂ) Int.cast_injective
[GOAL]
case a
n : ℕ
hpos : 0 < n
R : Type u_1
inst✝ : CommRing R
⊢ map (Int.castRingHom ℂ) (∏ i in Nat.divisors n, cyclotomic i ℤ) = map (Int.castRingHom ℂ) (X ^ n - 1)
[PROOFSTEP]
simp only [Polynomial.map_prod, int_cyclotomic_spec, Polynomial.map_pow, map_X, Polynomial.map_one, Polynomial.map_sub]
[GOAL]
case a
n : ℕ
hpos : 0 < n
R : Type u_1
inst✝ : CommRing R
⊢ ∏ x in Nat.divisors n, cyclotomic' x ℂ = X ^ n - 1
[PROOFSTEP]
exact prod_cyclotomic'_eq_X_pow_sub_one hpos (Complex.isPrimitiveRoot_exp n hpos.ne')
[GOAL]
n : ℕ
hpos : 0 < n
R : Type u_1
inst✝ : CommRing R
integer : ∏ i in Nat.divisors n, cyclotomic i ℤ = X ^ n - 1
⊢ ∏ i in Nat.divisors n, cyclotomic i R = X ^ n - 1
[PROOFSTEP]
simpa only [Polynomial.map_prod, map_cyclotomic_int, Polynomial.map_sub, Polynomial.map_one, Polynomial.map_pow,
  Polynomial.map_X] using congr_arg (map (Int.castRingHom R)) integer
[GOAL]
n : ℕ
R : Type u_1
inst✝ : Ring R
⊢ cyclotomic n R ∣ X ^ n - 1
[PROOFSTEP]
suffices cyclotomic n ℤ ∣ X ^ n - 1 by
  simpa only [map_cyclotomic_int, Polynomial.map_sub, Polynomial.map_one, Polynomial.map_pow, Polynomial.map_X] using
    map_dvd (Int.castRingHom R) this
[GOAL]
n : ℕ
R : Type u_1
inst✝ : Ring R
this : cyclotomic n ℤ ∣ X ^ n - 1
⊢ cyclotomic n R ∣ X ^ n - 1
[PROOFSTEP]
simpa only [map_cyclotomic_int, Polynomial.map_sub, Polynomial.map_one, Polynomial.map_pow, Polynomial.map_X] using
  map_dvd (Int.castRingHom R) this
[GOAL]
n : ℕ
R : Type u_1
inst✝ : Ring R
⊢ cyclotomic n ℤ ∣ X ^ n - 1
[PROOFSTEP]
rcases n.eq_zero_or_pos with (rfl | hn)
[GOAL]
case inl
R : Type u_1
inst✝ : Ring R
⊢ cyclotomic 0 ℤ ∣ X ^ 0 - 1
[PROOFSTEP]
simp
[GOAL]
case inr
n : ℕ
R : Type u_1
inst✝ : Ring R
hn : n > 0
⊢ cyclotomic n ℤ ∣ X ^ n - 1
[PROOFSTEP]
rw [← prod_cyclotomic_eq_X_pow_sub_one hn]
[GOAL]
case inr
n : ℕ
R : Type u_1
inst✝ : Ring R
hn : n > 0
⊢ cyclotomic n ℤ ∣ ∏ i in Nat.divisors n, cyclotomic i ℤ
[PROOFSTEP]
exact Finset.dvd_prod_of_mem _ (n.mem_divisors_self hn.ne')
[GOAL]
n : ℕ
h : 0 < n
R : Type u_1
inst✝ : CommRing R
⊢ ∏ i in Finset.erase (Nat.divisors n) 1, cyclotomic i R = ∑ i in range n, X ^ i
[PROOFSTEP]
suffices (∏ i in n.divisors.erase 1, cyclotomic i ℤ) = ∑ i in Finset.range n, X ^ i by
  simpa only [Polynomial.map_prod, map_cyclotomic_int, Polynomial.map_sum, Polynomial.map_pow, Polynomial.map_X] using
    congr_arg (map (Int.castRingHom R)) this
[GOAL]
n : ℕ
h : 0 < n
R : Type u_1
inst✝ : CommRing R
this : ∏ i in Finset.erase (Nat.divisors n) 1, cyclotomic i ℤ = ∑ i in range n, X ^ i
⊢ ∏ i in Finset.erase (Nat.divisors n) 1, cyclotomic i R = ∑ i in range n, X ^ i
[PROOFSTEP]
simpa only [Polynomial.map_prod, map_cyclotomic_int, Polynomial.map_sum, Polynomial.map_pow, Polynomial.map_X] using
  congr_arg (map (Int.castRingHom R)) this
[GOAL]
n : ℕ
h : 0 < n
R : Type u_1
inst✝ : CommRing R
⊢ ∏ i in Finset.erase (Nat.divisors n) 1, cyclotomic i ℤ = ∑ i in range n, X ^ i
[PROOFSTEP]
rw [← mul_left_inj' (cyclotomic_ne_zero 1 ℤ), prod_erase_mul _ _ (Nat.one_mem_divisors.2 h.ne'), cyclotomic_one,
  geom_sum_mul, prod_cyclotomic_eq_X_pow_sub_one h]
[GOAL]
R : Type u_1
inst✝ : Ring R
p : ℕ
hp : Fact (Nat.Prime p)
⊢ cyclotomic p R = ∑ i in range p, X ^ i
[PROOFSTEP]
suffices cyclotomic p ℤ = ∑ i in range p, X ^ i by
  simpa only [map_cyclotomic_int, Polynomial.map_sum, Polynomial.map_pow, Polynomial.map_X] using
    congr_arg (map (Int.castRingHom R)) this
[GOAL]
R : Type u_1
inst✝ : Ring R
p : ℕ
hp : Fact (Nat.Prime p)
this : cyclotomic p ℤ = ∑ i in range p, X ^ i
⊢ cyclotomic p R = ∑ i in range p, X ^ i
[PROOFSTEP]
simpa only [map_cyclotomic_int, Polynomial.map_sum, Polynomial.map_pow, Polynomial.map_X] using
  congr_arg (map (Int.castRingHom R)) this
[GOAL]
R : Type u_1
inst✝ : Ring R
p : ℕ
hp : Fact (Nat.Prime p)
⊢ cyclotomic p ℤ = ∑ i in range p, X ^ i
[PROOFSTEP]
rw [← prod_cyclotomic_eq_geom_sum hp.out.pos, hp.out.divisors, erase_insert (mem_singleton.not.2 hp.out.ne_one.symm),
  prod_singleton]
[GOAL]
R : Type u_1
inst✝ : Ring R
p : ℕ
hn : Fact (Nat.Prime p)
⊢ cyclotomic p R * (X - 1) = X ^ p - 1
[PROOFSTEP]
rw [cyclotomic_prime, geom_sum_mul]
[GOAL]
R : Type u_1
inst✝ : Ring R
⊢ cyclotomic 2 R = X + 1
[PROOFSTEP]
simp [cyclotomic_prime]
[GOAL]
R : Type u_1
inst✝ : Ring R
⊢ cyclotomic 3 R = X ^ 2 + X + 1
[PROOFSTEP]
simp [cyclotomic_prime, sum_range_succ']
[GOAL]
R : Type u_1
inst✝ : Ring R
d n : ℕ
hdn : d ∣ n
hd : d ≠ 1
⊢ cyclotomic d R ∣ ∑ i in range n, X ^ i
[PROOFSTEP]
suffices cyclotomic d ℤ ∣ ∑ i in Finset.range n, X ^ i by
  simpa only [map_cyclotomic_int, Polynomial.map_sum, Polynomial.map_pow, Polynomial.map_X] using
    map_dvd (Int.castRingHom R) this
[GOAL]
R : Type u_1
inst✝ : Ring R
d n : ℕ
hdn : d ∣ n
hd : d ≠ 1
this : cyclotomic d ℤ ∣ ∑ i in range n, X ^ i
⊢ cyclotomic d R ∣ ∑ i in range n, X ^ i
[PROOFSTEP]
simpa only [map_cyclotomic_int, Polynomial.map_sum, Polynomial.map_pow, Polynomial.map_X] using
  map_dvd (Int.castRingHom R) this
[GOAL]
R : Type u_1
inst✝ : Ring R
d n : ℕ
hdn : d ∣ n
hd : d ≠ 1
⊢ cyclotomic d ℤ ∣ ∑ i in range n, X ^ i
[PROOFSTEP]
rcases n.eq_zero_or_pos with (rfl | hn)
[GOAL]
case inl
R : Type u_1
inst✝ : Ring R
d : ℕ
hd : d ≠ 1
hdn : d ∣ 0
⊢ cyclotomic d ℤ ∣ ∑ i in range 0, X ^ i
[PROOFSTEP]
simp
[GOAL]
case inr
R : Type u_1
inst✝ : Ring R
d n : ℕ
hdn : d ∣ n
hd : d ≠ 1
hn : n > 0
⊢ cyclotomic d ℤ ∣ ∑ i in range n, X ^ i
[PROOFSTEP]
rw [← prod_cyclotomic_eq_geom_sum hn]
[GOAL]
case inr
R : Type u_1
inst✝ : Ring R
d n : ℕ
hdn : d ∣ n
hd : d ≠ 1
hn : n > 0
⊢ cyclotomic d ℤ ∣ ∏ i in Finset.erase (Nat.divisors n) 1, cyclotomic i ℤ
[PROOFSTEP]
apply Finset.dvd_prod_of_mem
[GOAL]
case inr.ha
R : Type u_1
inst✝ : Ring R
d n : ℕ
hdn : d ∣ n
hd : d ≠ 1
hn : n > 0
⊢ d ∈ Finset.erase (Nat.divisors n) 1
[PROOFSTEP]
simp [hd, hdn, hn.ne']
[GOAL]
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ Nat.properDivisors n
⊢ (X ^ d - 1) * ∏ x in Nat.divisors n \ Nat.divisors d, cyclotomic x R = X ^ n - 1
[PROOFSTEP]
obtain ⟨hd, hdn⟩ := Nat.mem_properDivisors.mp h
[GOAL]
case intro
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ Nat.properDivisors n
hd : d ∣ n
hdn : d < n
⊢ (X ^ d - 1) * ∏ x in Nat.divisors n \ Nat.divisors d, cyclotomic x R = X ^ n - 1
[PROOFSTEP]
have h0n : 0 < n := pos_of_gt hdn
[GOAL]
case intro
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ Nat.properDivisors n
hd : d ∣ n
hdn : d < n
h0n : 0 < n
⊢ (X ^ d - 1) * ∏ x in Nat.divisors n \ Nat.divisors d, cyclotomic x R = X ^ n - 1
[PROOFSTEP]
have h0d : 0 < d := Nat.pos_of_dvd_of_pos hd h0n
[GOAL]
case intro
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ Nat.properDivisors n
hd : d ∣ n
hdn : d < n
h0n : 0 < n
h0d : 0 < d
⊢ (X ^ d - 1) * ∏ x in Nat.divisors n \ Nat.divisors d, cyclotomic x R = X ^ n - 1
[PROOFSTEP]
rw [← prod_cyclotomic_eq_X_pow_sub_one h0d, ← prod_cyclotomic_eq_X_pow_sub_one h0n, mul_comm,
  Finset.prod_sdiff (Nat.divisors_subset_of_dvd h0n.ne' hd)]
[GOAL]
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ Nat.properDivisors n
⊢ (X ^ d - 1) * cyclotomic n R ∣ X ^ n - 1
[PROOFSTEP]
have hdn := (Nat.mem_properDivisors.mp h).2
[GOAL]
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ Nat.properDivisors n
hdn : d < n
⊢ (X ^ d - 1) * cyclotomic n R ∣ X ^ n - 1
[PROOFSTEP]
use∏ x in n.properDivisors \ d.divisors, cyclotomic x R
[GOAL]
case h
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ Nat.properDivisors n
hdn : d < n
⊢ X ^ n - 1 = (X ^ d - 1) * cyclotomic n R * ∏ x in Nat.properDivisors n \ Nat.divisors d, cyclotomic x R
[PROOFSTEP]
symm
[GOAL]
case h
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ Nat.properDivisors n
hdn : d < n
⊢ (X ^ d - 1) * cyclotomic n R * ∏ x in Nat.properDivisors n \ Nat.divisors d, cyclotomic x R = X ^ n - 1
[PROOFSTEP]
convert X_pow_sub_one_mul_prod_cyclotomic_eq_X_pow_sub_one_of_dvd R h using 1
[GOAL]
case h.e'_2
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ Nat.properDivisors n
hdn : d < n
⊢ (X ^ d - 1) * cyclotomic n R * ∏ x in Nat.properDivisors n \ Nat.divisors d, cyclotomic x R =
    (X ^ d - 1) * ∏ x in Nat.divisors n \ Nat.divisors d, cyclotomic x R
[PROOFSTEP]
rw [mul_assoc]
[GOAL]
case h.e'_2
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ Nat.properDivisors n
hdn : d < n
⊢ (X ^ d - 1) * (cyclotomic n R * ∏ x in Nat.properDivisors n \ Nat.divisors d, cyclotomic x R) =
    (X ^ d - 1) * ∏ x in Nat.divisors n \ Nat.divisors d, cyclotomic x R
[PROOFSTEP]
congr 1
[GOAL]
case h.e'_2.e_a
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ Nat.properDivisors n
hdn : d < n
⊢ cyclotomic n R * ∏ x in Nat.properDivisors n \ Nat.divisors d, cyclotomic x R =
    ∏ x in Nat.divisors n \ Nat.divisors d, cyclotomic x R
[PROOFSTEP]
rw [← Nat.insert_self_properDivisors hdn.ne_bot, insert_sdiff_of_not_mem, prod_insert]
[GOAL]
case h.e'_2.e_a
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ Nat.properDivisors n
hdn : d < n
⊢ ¬n ∈ Nat.properDivisors n \ Nat.divisors d
[PROOFSTEP]
exact Finset.not_mem_sdiff_of_not_mem_left Nat.properDivisors.not_self_mem
[GOAL]
case h.e'_2.e_a.h
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ Nat.properDivisors n
hdn : d < n
⊢ ¬n ∈ Nat.divisors d
[PROOFSTEP]
exact fun hk => hdn.not_le <| Nat.divisor_le hk
[GOAL]
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ ↑(algebraMap R[X] (RatFunc R)) (cyclotomic n R) =
    ∏ i in Nat.divisorsAntidiagonal n, ↑(algebraMap R[X] (RatFunc R)) (X ^ i.snd - 1) ^ ↑μ i.fst
[PROOFSTEP]
rcases n.eq_zero_or_pos with (rfl | hpos)
[GOAL]
case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ ↑(algebraMap R[X] (RatFunc R)) (cyclotomic 0 R) =
    ∏ i in Nat.divisorsAntidiagonal 0, ↑(algebraMap R[X] (RatFunc R)) (X ^ i.snd - 1) ^ ↑μ i.fst
[PROOFSTEP]
simp
[GOAL]
case inr
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hpos : n > 0
⊢ ↑(algebraMap R[X] (RatFunc R)) (cyclotomic n R) =
    ∏ i in Nat.divisorsAntidiagonal n, ↑(algebraMap R[X] (RatFunc R)) (X ^ i.snd - 1) ^ ↑μ i.fst
[PROOFSTEP]
have h :
  ∀ n : ℕ,
    0 < n → (∏ i in Nat.divisors n, algebraMap _ (RatFunc R) (cyclotomic i R)) = algebraMap _ _ (X ^ n - 1 : R[X]) :=
  by
  intro n hn
  rw [← prod_cyclotomic_eq_X_pow_sub_one hn R, map_prod]
[GOAL]
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hpos : n > 0
⊢ ∀ (n : ℕ),
    0 < n →
      ∏ i in Nat.divisors n, ↑(algebraMap R[X] (RatFunc R)) (cyclotomic i R) =
        ↑(algebraMap R[X] (RatFunc R)) (X ^ n - 1)
[PROOFSTEP]
intro n hn
[GOAL]
n✝ : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hpos : n✝ > 0
n : ℕ
hn : 0 < n
⊢ ∏ i in Nat.divisors n, ↑(algebraMap R[X] (RatFunc R)) (cyclotomic i R) = ↑(algebraMap R[X] (RatFunc R)) (X ^ n - 1)
[PROOFSTEP]
rw [← prod_cyclotomic_eq_X_pow_sub_one hn R, map_prod]
[GOAL]
case inr
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hpos : n > 0
h :
  ∀ (n : ℕ),
    0 < n →
      ∏ i in Nat.divisors n, ↑(algebraMap R[X] (RatFunc R)) (cyclotomic i R) =
        ↑(algebraMap R[X] (RatFunc R)) (X ^ n - 1)
⊢ ↑(algebraMap R[X] (RatFunc R)) (cyclotomic n R) =
    ∏ i in Nat.divisorsAntidiagonal n, ↑(algebraMap R[X] (RatFunc R)) (X ^ i.snd - 1) ^ ↑μ i.fst
[PROOFSTEP]
rw [(prod_eq_iff_prod_pow_moebius_eq_of_nonzero (fun n hn => _) fun n hn => _).1 h n hpos]
[GOAL]
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hpos : n > 0
h :
  ∀ (n : ℕ),
    0 < n →
      ∏ i in Nat.divisors n, ↑(algebraMap R[X] (RatFunc R)) (cyclotomic i R) =
        ↑(algebraMap R[X] (RatFunc R)) (X ^ n - 1)
⊢ ∀ (n : ℕ), 0 < n → ↑(algebraMap R[X] (RatFunc R)) (cyclotomic n R) ≠ 0
[PROOFSTEP]
simp_rw [Ne.def, IsFractionRing.to_map_eq_zero_iff]
[GOAL]
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hpos : n > 0
h :
  ∀ (n : ℕ),
    0 < n →
      ∏ i in Nat.divisors n, ↑(algebraMap R[X] (RatFunc R)) (cyclotomic i R) =
        ↑(algebraMap R[X] (RatFunc R)) (X ^ n - 1)
⊢ ∀ (n : ℕ), 0 < n → ↑(algebraMap R[X] (RatFunc R)) (X ^ n - 1) ≠ 0
[PROOFSTEP]
simp_rw [Ne.def, IsFractionRing.to_map_eq_zero_iff]
[GOAL]
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hpos : n > 0
h :
  ∀ (n : ℕ),
    0 < n →
      ∏ i in Nat.divisors n, ↑(algebraMap R[X] (RatFunc R)) (cyclotomic i R) =
        ↑(algebraMap R[X] (RatFunc R)) (X ^ n - 1)
⊢ ∀ (n : ℕ), 0 < n → ¬cyclotomic n R = 0
[PROOFSTEP]
simp [cyclotomic_ne_zero]
[GOAL]
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hpos : n > 0
h :
  ∀ (n : ℕ),
    0 < n →
      ∏ i in Nat.divisors n, ↑(algebraMap R[X] (RatFunc R)) (cyclotomic i R) =
        ↑(algebraMap R[X] (RatFunc R)) (X ^ n - 1)
⊢ ∀ (n : ℕ), 0 < n → ¬X ^ n - 1 = 0
[PROOFSTEP]
intro n hn
[GOAL]
n✝ : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hpos : n✝ > 0
h :
  ∀ (n : ℕ),
    0 < n →
      ∏ i in Nat.divisors n, ↑(algebraMap R[X] (RatFunc R)) (cyclotomic i R) =
        ↑(algebraMap R[X] (RatFunc R)) (X ^ n - 1)
n : ℕ
hn : 0 < n
⊢ ¬X ^ n - 1 = 0
[PROOFSTEP]
apply Monic.ne_zero
[GOAL]
case hp
n✝ : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hpos : n✝ > 0
h :
  ∀ (n : ℕ),
    0 < n →
      ∏ i in Nat.divisors n, ↑(algebraMap R[X] (RatFunc R)) (cyclotomic i R) =
        ↑(algebraMap R[X] (RatFunc R)) (X ^ n - 1)
n : ℕ
hn : 0 < n
⊢ Monic (X ^ n - 1)
[PROOFSTEP]
apply monic_X_pow_sub_C _ (ne_of_gt hn)
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
⊢ cyclotomic n R = (X ^ n - 1) /ₘ ∏ i in Nat.properDivisors n, cyclotomic i R
[PROOFSTEP]
nontriviality R
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
✝ : Nontrivial R
⊢ cyclotomic n R = (X ^ n - 1) /ₘ ∏ i in Nat.properDivisors n, cyclotomic i R
[PROOFSTEP]
rw [← prod_cyclotomic_eq_X_pow_sub_one hpos, ← Nat.cons_self_properDivisors hpos.ne', Finset.prod_cons]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
✝ : Nontrivial R
⊢ cyclotomic n R =
    (cyclotomic n R * ∏ x in Nat.properDivisors n, cyclotomic x R) /ₘ ∏ i in Nat.properDivisors n, cyclotomic i R
[PROOFSTEP]
have prod_monic : (∏ i in Nat.properDivisors n, cyclotomic i R).Monic :=
  by
  apply monic_prod_of_monic
  intro i _
  exact cyclotomic.monic i R
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
✝ : Nontrivial R
⊢ Monic (∏ i in Nat.properDivisors n, cyclotomic i R)
[PROOFSTEP]
apply monic_prod_of_monic
[GOAL]
case hs
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
✝ : Nontrivial R
⊢ ∀ (i : ℕ), i ∈ Nat.properDivisors n → Monic (cyclotomic i R)
[PROOFSTEP]
intro i _
[GOAL]
case hs
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
✝ : Nontrivial R
i : ℕ
a✝ : i ∈ Nat.properDivisors n
⊢ Monic (cyclotomic i R)
[PROOFSTEP]
exact cyclotomic.monic i R
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
✝ : Nontrivial R
prod_monic : Monic (∏ i in Nat.properDivisors n, cyclotomic i R)
⊢ cyclotomic n R =
    (cyclotomic n R * ∏ x in Nat.properDivisors n, cyclotomic x R) /ₘ ∏ i in Nat.properDivisors n, cyclotomic i R
[PROOFSTEP]
rw [(div_modByMonic_unique (cyclotomic n R) 0 prod_monic _).1]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
✝ : Nontrivial R
prod_monic : Monic (∏ i in Nat.properDivisors n, cyclotomic i R)
⊢ 0 + (∏ i in Nat.properDivisors n, cyclotomic i R) * cyclotomic n R =
      cyclotomic n R * ∏ x in Nat.properDivisors n, cyclotomic x R ∧
    degree 0 < degree (∏ i in Nat.properDivisors n, cyclotomic i R)
[PROOFSTEP]
simp only [degree_zero, zero_add]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
✝ : Nontrivial R
prod_monic : Monic (∏ i in Nat.properDivisors n, cyclotomic i R)
⊢ (∏ i in Nat.properDivisors n, cyclotomic i R) * cyclotomic n R =
      cyclotomic n R * ∏ i in Nat.properDivisors n, cyclotomic i R ∧
    ⊥ < degree (∏ i in Nat.properDivisors n, cyclotomic i R)
[PROOFSTEP]
constructor
[GOAL]
case left
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
✝ : Nontrivial R
prod_monic : Monic (∏ i in Nat.properDivisors n, cyclotomic i R)
⊢ (∏ i in Nat.properDivisors n, cyclotomic i R) * cyclotomic n R =
    cyclotomic n R * ∏ i in Nat.properDivisors n, cyclotomic i R
[PROOFSTEP]
rw [mul_comm]
[GOAL]
case right
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
✝ : Nontrivial R
prod_monic : Monic (∏ i in Nat.properDivisors n, cyclotomic i R)
⊢ ⊥ < degree (∏ i in Nat.properDivisors n, cyclotomic i R)
[PROOFSTEP]
rw [bot_lt_iff_ne_bot]
[GOAL]
case right
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
✝ : Nontrivial R
prod_monic : Monic (∏ i in Nat.properDivisors n, cyclotomic i R)
⊢ degree (∏ i in Nat.properDivisors n, cyclotomic i R) ≠ ⊥
[PROOFSTEP]
intro h
[GOAL]
case right
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
✝ : Nontrivial R
prod_monic : Monic (∏ i in Nat.properDivisors n, cyclotomic i R)
h : degree (∏ i in Nat.properDivisors n, cyclotomic i R) = ⊥
⊢ False
[PROOFSTEP]
exact Monic.ne_zero prod_monic (degree_eq_bot.1 h)
[GOAL]
R : Type u_1
inst✝ : CommRing R
n m : ℕ
hpos : 0 < n
hm : m ∣ n
hdiff : m ≠ n
⊢ X ^ m - 1 ∣ ∏ i in Nat.properDivisors n, cyclotomic i R
[PROOFSTEP]
replace hm := Nat.mem_properDivisors.2 ⟨hm, lt_of_le_of_ne (Nat.divisor_le (Nat.mem_divisors.2 ⟨hm, hpos.ne'⟩)) hdiff⟩
[GOAL]
R : Type u_1
inst✝ : CommRing R
n m : ℕ
hpos : 0 < n
hdiff : m ≠ n
hm : m ∈ Nat.properDivisors n
⊢ X ^ m - 1 ∣ ∏ i in Nat.properDivisors n, cyclotomic i R
[PROOFSTEP]
rw [←
  Finset.sdiff_union_of_subset
    (Nat.divisors_subset_properDivisors (ne_of_lt hpos).symm (Nat.mem_properDivisors.1 hm).1
      (ne_of_lt (Nat.mem_properDivisors.1 hm).2)),
  Finset.prod_union Finset.sdiff_disjoint, prod_cyclotomic_eq_X_pow_sub_one (Nat.pos_of_mem_properDivisors hm)]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n m : ℕ
hpos : 0 < n
hdiff : m ≠ n
hm : m ∈ Nat.properDivisors n
⊢ X ^ m - 1 ∣ (∏ x in Nat.properDivisors n \ Nat.divisors m, cyclotomic x R) * (X ^ m - 1)
[PROOFSTEP]
exact ⟨∏ x : ℕ in n.properDivisors \ m.divisors, cyclotomic x R, by rw [mul_comm]⟩
[GOAL]
R : Type u_1
inst✝ : CommRing R
n m : ℕ
hpos : 0 < n
hdiff : m ≠ n
hm : m ∈ Nat.properDivisors n
⊢ (∏ x in Nat.properDivisors n \ Nat.divisors m, cyclotomic x R) * (X ^ m - 1) =
    (X ^ m - 1) * ∏ x in Nat.properDivisors n \ Nat.divisors m, cyclotomic x R
[PROOFSTEP]
rw [mul_comm]
[GOAL]
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hz : IsPrimitiveRoot ζ n
⊢ cyclotomic n K = ∏ μ in primitiveRoots n K, (X - ↑C μ)
[PROOFSTEP]
rw [← cyclotomic']
[GOAL]
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hz : IsPrimitiveRoot ζ n
⊢ cyclotomic n K = cyclotomic' n K
[PROOFSTEP]
induction' n using Nat.strong_induction_on with k hk generalizing ζ
[GOAL]
case h
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
hz✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
hk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic m K = cyclotomic' m K
ζ : K
hz : IsPrimitiveRoot ζ k
⊢ cyclotomic k K = cyclotomic' k K
[PROOFSTEP]
obtain hzero | hpos := k.eq_zero_or_pos
[GOAL]
case h.inl
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
hz✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
hk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic m K = cyclotomic' m K
ζ : K
hz : IsPrimitiveRoot ζ k
hzero : k = 0
⊢ cyclotomic k K = cyclotomic' k K
[PROOFSTEP]
simp only [hzero, cyclotomic'_zero, cyclotomic_zero]
[GOAL]
case h.inr
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
hz✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
hk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic m K = cyclotomic' m K
ζ : K
hz : IsPrimitiveRoot ζ k
hpos : k > 0
⊢ cyclotomic k K = cyclotomic' k K
[PROOFSTEP]
have h : ∀ i ∈ k.properDivisors, cyclotomic i K = cyclotomic' i K :=
  by
  intro i hi
  obtain ⟨d, hd⟩ := (Nat.mem_properDivisors.1 hi).1
  rw [mul_comm] at hd
  exact hk i (Nat.mem_properDivisors.1 hi).2 (IsPrimitiveRoot.pow hpos hz hd)
[GOAL]
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
hz✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
hk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic m K = cyclotomic' m K
ζ : K
hz : IsPrimitiveRoot ζ k
hpos : k > 0
⊢ ∀ (i : ℕ), i ∈ Nat.properDivisors k → cyclotomic i K = cyclotomic' i K
[PROOFSTEP]
intro i hi
[GOAL]
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
hz✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
hk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic m K = cyclotomic' m K
ζ : K
hz : IsPrimitiveRoot ζ k
hpos : k > 0
i : ℕ
hi : i ∈ Nat.properDivisors k
⊢ cyclotomic i K = cyclotomic' i K
[PROOFSTEP]
obtain ⟨d, hd⟩ := (Nat.mem_properDivisors.1 hi).1
[GOAL]
case intro
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
hz✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
hk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic m K = cyclotomic' m K
ζ : K
hz : IsPrimitiveRoot ζ k
hpos : k > 0
i : ℕ
hi : i ∈ Nat.properDivisors k
d : ℕ
hd : k = i * d
⊢ cyclotomic i K = cyclotomic' i K
[PROOFSTEP]
rw [mul_comm] at hd
[GOAL]
case intro
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
hz✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
hk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic m K = cyclotomic' m K
ζ : K
hz : IsPrimitiveRoot ζ k
hpos : k > 0
i : ℕ
hi : i ∈ Nat.properDivisors k
d : ℕ
hd : k = d * i
⊢ cyclotomic i K = cyclotomic' i K
[PROOFSTEP]
exact hk i (Nat.mem_properDivisors.1 hi).2 (IsPrimitiveRoot.pow hpos hz hd)
[GOAL]
case h.inr
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ✝ : K
n : ℕ
hz✝ : IsPrimitiveRoot ζ✝ n
k : ℕ
hk : ∀ (m : ℕ), m < k → ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic m K = cyclotomic' m K
ζ : K
hz : IsPrimitiveRoot ζ k
hpos : k > 0
h : ∀ (i : ℕ), i ∈ Nat.properDivisors k → cyclotomic i K = cyclotomic' i K
⊢ cyclotomic k K = cyclotomic' k K
[PROOFSTEP]
rw [@cyclotomic_eq_X_pow_sub_one_div _ _ _ hpos, cyclotomic'_eq_X_pow_sub_one_div hpos hz,
  Finset.prod_congr (refl k.properDivisors) h]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
⊢ P = cyclotomic n R ↔ P * ∏ i in Nat.properDivisors n, cyclotomic i R = X ^ n - 1
[PROOFSTEP]
nontriviality R
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
✝ : Nontrivial R
⊢ P = cyclotomic n R ↔ P * ∏ i in Nat.properDivisors n, cyclotomic i R = X ^ n - 1
[PROOFSTEP]
refine' ⟨fun hcycl => _, fun hP => _⟩
[GOAL]
case refine'_1
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
✝ : Nontrivial R
hcycl : P = cyclotomic n R
⊢ P * ∏ i in Nat.properDivisors n, cyclotomic i R = X ^ n - 1
[PROOFSTEP]
rw [hcycl, ← prod_cyclotomic_eq_X_pow_sub_one hpos R, ← Nat.cons_self_properDivisors hpos.ne', Finset.prod_cons]
[GOAL]
case refine'_2
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
✝ : Nontrivial R
hP : P * ∏ i in Nat.properDivisors n, cyclotomic i R = X ^ n - 1
⊢ P = cyclotomic n R
[PROOFSTEP]
have prod_monic : (∏ i in Nat.properDivisors n, cyclotomic i R).Monic :=
  by
  apply monic_prod_of_monic
  intro i _
  exact cyclotomic.monic i R
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
✝ : Nontrivial R
hP : P * ∏ i in Nat.properDivisors n, cyclotomic i R = X ^ n - 1
⊢ Monic (∏ i in Nat.properDivisors n, cyclotomic i R)
[PROOFSTEP]
apply monic_prod_of_monic
[GOAL]
case hs
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
✝ : Nontrivial R
hP : P * ∏ i in Nat.properDivisors n, cyclotomic i R = X ^ n - 1
⊢ ∀ (i : ℕ), i ∈ Nat.properDivisors n → Monic (cyclotomic i R)
[PROOFSTEP]
intro i _
[GOAL]
case hs
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
✝ : Nontrivial R
hP : P * ∏ i in Nat.properDivisors n, cyclotomic i R = X ^ n - 1
i : ℕ
a✝ : i ∈ Nat.properDivisors n
⊢ Monic (cyclotomic i R)
[PROOFSTEP]
exact cyclotomic.monic i R
[GOAL]
case refine'_2
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
✝ : Nontrivial R
hP : P * ∏ i in Nat.properDivisors n, cyclotomic i R = X ^ n - 1
prod_monic : Monic (∏ i in Nat.properDivisors n, cyclotomic i R)
⊢ P = cyclotomic n R
[PROOFSTEP]
rw [@cyclotomic_eq_X_pow_sub_one_div R _ _ hpos, (div_modByMonic_unique P 0 prod_monic _).1]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
✝ : Nontrivial R
hP : P * ∏ i in Nat.properDivisors n, cyclotomic i R = X ^ n - 1
prod_monic : Monic (∏ i in Nat.properDivisors n, cyclotomic i R)
⊢ 0 + (∏ i in Nat.properDivisors n, cyclotomic i R) * P = X ^ n - 1 ∧
    degree 0 < degree (∏ i in Nat.properDivisors n, cyclotomic i R)
[PROOFSTEP]
refine' ⟨by rwa [zero_add, mul_comm], _⟩
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
✝ : Nontrivial R
hP : P * ∏ i in Nat.properDivisors n, cyclotomic i R = X ^ n - 1
prod_monic : Monic (∏ i in Nat.properDivisors n, cyclotomic i R)
⊢ 0 + (∏ i in Nat.properDivisors n, cyclotomic i R) * P = X ^ n - 1
[PROOFSTEP]
rwa [zero_add, mul_comm]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
✝ : Nontrivial R
hP : P * ∏ i in Nat.properDivisors n, cyclotomic i R = X ^ n - 1
prod_monic : Monic (∏ i in Nat.properDivisors n, cyclotomic i R)
⊢ degree 0 < degree (∏ i in Nat.properDivisors n, cyclotomic i R)
[PROOFSTEP]
rw [degree_zero, bot_lt_iff_ne_bot]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
✝ : Nontrivial R
hP : P * ∏ i in Nat.properDivisors n, cyclotomic i R = X ^ n - 1
prod_monic : Monic (∏ i in Nat.properDivisors n, cyclotomic i R)
⊢ degree (∏ i in Nat.properDivisors n, cyclotomic i R) ≠ ⊥
[PROOFSTEP]
intro h
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
✝ : Nontrivial R
hP : P * ∏ i in Nat.properDivisors n, cyclotomic i R = X ^ n - 1
prod_monic : Monic (∏ i in Nat.properDivisors n, cyclotomic i R)
h : degree (∏ i in Nat.properDivisors n, cyclotomic i R) = ⊥
⊢ False
[PROOFSTEP]
exact Monic.ne_zero prod_monic (degree_eq_bot.1 h)
[GOAL]
R : Type u_1
inst✝ : CommRing R
p n : ℕ
hp : Nat.Prime p
⊢ cyclotomic (p ^ (n + 1)) R = ∑ i in range p, (X ^ p ^ n) ^ i
[PROOFSTEP]
have :
  ∀ m,
    (cyclotomic (p ^ (m + 1)) R = ∑ i in Finset.range p, (X ^ p ^ m) ^ i) ↔
      ((∑ i in Finset.range p, (X ^ p ^ m) ^ i) * ∏ x : ℕ in Finset.range (m + 1), cyclotomic (p ^ x) R) =
        X ^ p ^ (m + 1) - 1 :=
  by
  intro m
  have := eq_cyclotomic_iff (R := R) (P := ∑ i in range p, (X ^ p ^ m) ^ i) (pow_pos hp.pos (m + 1))
  rw [eq_comm] at this
  rw [this, Nat.prod_properDivisors_prime_pow hp]
[GOAL]
R : Type u_1
inst✝ : CommRing R
p n : ℕ
hp : Nat.Prime p
⊢ ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i in range p, (X ^ p ^ m) ^ i ↔
      (∑ i in range p, (X ^ p ^ m) ^ i) * ∏ x in range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
[PROOFSTEP]
intro m
[GOAL]
R : Type u_1
inst✝ : CommRing R
p n : ℕ
hp : Nat.Prime p
m : ℕ
⊢ cyclotomic (p ^ (m + 1)) R = ∑ i in range p, (X ^ p ^ m) ^ i ↔
    (∑ i in range p, (X ^ p ^ m) ^ i) * ∏ x in range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
[PROOFSTEP]
have := eq_cyclotomic_iff (R := R) (P := ∑ i in range p, (X ^ p ^ m) ^ i) (pow_pos hp.pos (m + 1))
[GOAL]
R : Type u_1
inst✝ : CommRing R
p n : ℕ
hp : Nat.Prime p
m : ℕ
this :
  ∑ i in range p, (X ^ p ^ m) ^ i = cyclotomic (p ^ (m + 1)) R ↔
    (∑ i in range p, (X ^ p ^ m) ^ i) * ∏ i in Nat.properDivisors (p ^ (m + 1)), cyclotomic i R = X ^ p ^ (m + 1) - 1
⊢ cyclotomic (p ^ (m + 1)) R = ∑ i in range p, (X ^ p ^ m) ^ i ↔
    (∑ i in range p, (X ^ p ^ m) ^ i) * ∏ x in range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
[PROOFSTEP]
rw [eq_comm] at this
[GOAL]
R : Type u_1
inst✝ : CommRing R
p n : ℕ
hp : Nat.Prime p
m : ℕ
this :
  cyclotomic (p ^ (m + 1)) R = ∑ i in range p, (X ^ p ^ m) ^ i ↔
    (∑ i in range p, (X ^ p ^ m) ^ i) * ∏ i in Nat.properDivisors (p ^ (m + 1)), cyclotomic i R = X ^ p ^ (m + 1) - 1
⊢ cyclotomic (p ^ (m + 1)) R = ∑ i in range p, (X ^ p ^ m) ^ i ↔
    (∑ i in range p, (X ^ p ^ m) ^ i) * ∏ x in range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
[PROOFSTEP]
rw [this, Nat.prod_properDivisors_prime_pow hp]
[GOAL]
R : Type u_1
inst✝ : CommRing R
p n : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i in range p, (X ^ p ^ m) ^ i ↔
      (∑ i in range p, (X ^ p ^ m) ^ i) * ∏ x in range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
⊢ cyclotomic (p ^ (n + 1)) R = ∑ i in range p, (X ^ p ^ n) ^ i
[PROOFSTEP]
induction' n with n_n n_ih
[GOAL]
case zero
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i in range p, (X ^ p ^ m) ^ i ↔
      (∑ i in range p, (X ^ p ^ m) ^ i) * ∏ x in range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
⊢ cyclotomic (p ^ (Nat.zero + 1)) R = ∑ i in range p, (X ^ p ^ Nat.zero) ^ i
[PROOFSTEP]
haveI := Fact.mk hp
[GOAL]
case zero
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
this✝ :
  ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i in range p, (X ^ p ^ m) ^ i ↔
      (∑ i in range p, (X ^ p ^ m) ^ i) * ∏ x in range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
this : Fact (Nat.Prime p)
⊢ cyclotomic (p ^ (Nat.zero + 1)) R = ∑ i in range p, (X ^ p ^ Nat.zero) ^ i
[PROOFSTEP]
simp [cyclotomic_prime]
[GOAL]
case succ
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i in range p, (X ^ p ^ m) ^ i ↔
      (∑ i in range p, (X ^ p ^ m) ^ i) * ∏ x in range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
n_n : ℕ
n_ih : cyclotomic (p ^ (n_n + 1)) R = ∑ i in range p, (X ^ p ^ n_n) ^ i
⊢ cyclotomic (p ^ (Nat.succ n_n + 1)) R = ∑ i in range p, (X ^ p ^ Nat.succ n_n) ^ i
[PROOFSTEP]
rw [((eq_cyclotomic_iff (pow_pos hp.pos (n_n.succ + 1)) _).mpr _).symm]
[GOAL]
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i in range p, (X ^ p ^ m) ^ i ↔
      (∑ i in range p, (X ^ p ^ m) ^ i) * ∏ x in range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
n_n : ℕ
n_ih : cyclotomic (p ^ (n_n + 1)) R = ∑ i in range p, (X ^ p ^ n_n) ^ i
⊢ (∑ i in range p, (X ^ p ^ Nat.succ n_n) ^ i) * ∏ i in Nat.properDivisors (p ^ (Nat.succ n_n + 1)), cyclotomic i R =
    X ^ p ^ (Nat.succ n_n + 1) - 1
[PROOFSTEP]
rw [Nat.prod_properDivisors_prime_pow hp, Finset.prod_range_succ, n_ih]
[GOAL]
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i in range p, (X ^ p ^ m) ^ i ↔
      (∑ i in range p, (X ^ p ^ m) ^ i) * ∏ x in range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
n_n : ℕ
n_ih : cyclotomic (p ^ (n_n + 1)) R = ∑ i in range p, (X ^ p ^ n_n) ^ i
⊢ (∑ i in range p, (X ^ p ^ Nat.succ n_n) ^ i) *
      ((∏ x in range (n_n + 1), cyclotomic (p ^ x) R) * ∑ i in range p, (X ^ p ^ n_n) ^ i) =
    X ^ p ^ (Nat.succ n_n + 1) - 1
[PROOFSTEP]
rw [this] at n_ih
[GOAL]
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i in range p, (X ^ p ^ m) ^ i ↔
      (∑ i in range p, (X ^ p ^ m) ^ i) * ∏ x in range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
n_n : ℕ
n_ih : (∑ i in range p, (X ^ p ^ n_n) ^ i) * ∏ x in range (n_n + 1), cyclotomic (p ^ x) R = X ^ p ^ (n_n + 1) - 1
⊢ (∑ i in range p, (X ^ p ^ Nat.succ n_n) ^ i) *
      ((∏ x in range (n_n + 1), cyclotomic (p ^ x) R) * ∑ i in range p, (X ^ p ^ n_n) ^ i) =
    X ^ p ^ (Nat.succ n_n + 1) - 1
[PROOFSTEP]
rw [mul_comm _ (∑ i in _, _), n_ih, geom_sum_mul, sub_left_inj, ← pow_mul, pow_add, pow_one]
[GOAL]
R : Type u_1
inst✝ : CommRing R
p k : ℕ
hn : Fact (Nat.Prime p)
⊢ cyclotomic (p ^ (k + 1)) R * (X ^ p ^ k - 1) = X ^ p ^ (k + 1) - 1
[PROOFSTEP]
rw [cyclotomic_prime_pow_eq_geom_sum hn.out, geom_sum_mul, ← pow_mul, pow_succ, mul_comm]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : 1 < n
⊢ coeff (cyclotomic n R) 0 = 1
[PROOFSTEP]
induction' n using Nat.strong_induction_on with n hi
[GOAL]
case h
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
hn✝ : 1 < n✝
n : ℕ
hi : ∀ (m : ℕ), m < n → 1 < m → coeff (cyclotomic m R) 0 = 1
hn : 1 < n
⊢ coeff (cyclotomic n R) 0 = 1
[PROOFSTEP]
have hprod : (∏ i in Nat.properDivisors n, (Polynomial.cyclotomic i R).coeff 0) = -1 :=
  by
  rw [← Finset.insert_erase (Nat.one_mem_properDivisors_iff_one_lt.2 (lt_of_lt_of_le one_lt_two hn)),
    Finset.prod_insert (Finset.not_mem_erase 1 _), cyclotomic_one R]
  have hleq : ∀ j ∈ n.properDivisors.erase 1, 2 ≤ j := by
    intro j hj
    apply Nat.succ_le_of_lt
    exact
      (Ne.le_iff_lt (Finset.mem_erase.1 hj).1.symm).mp
        (Nat.succ_le_of_lt (Nat.pos_of_mem_properDivisors (Finset.mem_erase.1 hj).2))
  have hcongr : ∀ j ∈ n.properDivisors.erase 1, (cyclotomic j R).coeff 0 = 1 :=
    by
    intro j hj
    exact hi j (Nat.mem_properDivisors.1 (Finset.mem_erase.1 hj).2).2 (hleq j hj)
  have hrw : (∏ x : ℕ in n.properDivisors.erase 1, (cyclotomic x R).coeff 0) = 1 :=
    by
    rw [Finset.prod_congr (refl (n.properDivisors.erase 1)) hcongr]
    simp only [Finset.prod_const_one]
  simp only [hrw, mul_one, zero_sub, coeff_one_zero, coeff_X_zero, coeff_sub]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
hn✝ : 1 < n✝
n : ℕ
hi : ∀ (m : ℕ), m < n → 1 < m → coeff (cyclotomic m R) 0 = 1
hn : 1 < n
⊢ ∏ i in Nat.properDivisors n, coeff (cyclotomic i R) 0 = -1
[PROOFSTEP]
rw [← Finset.insert_erase (Nat.one_mem_properDivisors_iff_one_lt.2 (lt_of_lt_of_le one_lt_two hn)),
  Finset.prod_insert (Finset.not_mem_erase 1 _), cyclotomic_one R]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
hn✝ : 1 < n✝
n : ℕ
hi : ∀ (m : ℕ), m < n → 1 < m → coeff (cyclotomic m R) 0 = 1
hn : 1 < n
⊢ coeff (X - 1) 0 * ∏ x in Finset.erase (Nat.properDivisors n) 1, coeff (cyclotomic x R) 0 = -1
[PROOFSTEP]
have hleq : ∀ j ∈ n.properDivisors.erase 1, 2 ≤ j := by
  intro j hj
  apply Nat.succ_le_of_lt
  exact
    (Ne.le_iff_lt (Finset.mem_erase.1 hj).1.symm).mp
      (Nat.succ_le_of_lt (Nat.pos_of_mem_properDivisors (Finset.mem_erase.1 hj).2))
[GOAL]
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
hn✝ : 1 < n✝
n : ℕ
hi : ∀ (m : ℕ), m < n → 1 < m → coeff (cyclotomic m R) 0 = 1
hn : 1 < n
⊢ ∀ (j : ℕ), j ∈ Finset.erase (Nat.properDivisors n) 1 → 2 ≤ j
[PROOFSTEP]
intro j hj
[GOAL]
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
hn✝ : 1 < n✝
n : ℕ
hi : ∀ (m : ℕ), m < n → 1 < m → coeff (cyclotomic m R) 0 = 1
hn : 1 < n
j : ℕ
hj : j ∈ Finset.erase (Nat.properDivisors n) 1
⊢ 2 ≤ j
[PROOFSTEP]
apply Nat.succ_le_of_lt
[GOAL]
case h
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
hn✝ : 1 < n✝
n : ℕ
hi : ∀ (m : ℕ), m < n → 1 < m → coeff (cyclotomic m R) 0 = 1
hn : 1 < n
j : ℕ
hj : j ∈ Finset.erase (Nat.properDivisors n) 1
⊢ 1 < j
[PROOFSTEP]
exact
  (Ne.le_iff_lt (Finset.mem_erase.1 hj).1.symm).mp
    (Nat.succ_le_of_lt (Nat.pos_of_mem_properDivisors (Finset.mem_erase.1 hj).2))
[GOAL]
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
hn✝ : 1 < n✝
n : ℕ
hi : ∀ (m : ℕ), m < n → 1 < m → coeff (cyclotomic m R) 0 = 1
hn : 1 < n
hleq : ∀ (j : ℕ), j ∈ Finset.erase (Nat.properDivisors n) 1 → 2 ≤ j
⊢ coeff (X - 1) 0 * ∏ x in Finset.erase (Nat.properDivisors n) 1, coeff (cyclotomic x R) 0 = -1
[PROOFSTEP]
have hcongr : ∀ j ∈ n.properDivisors.erase 1, (cyclotomic j R).coeff 0 = 1 :=
  by
  intro j hj
  exact hi j (Nat.mem_properDivisors.1 (Finset.mem_erase.1 hj).2).2 (hleq j hj)
[GOAL]
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
hn✝ : 1 < n✝
n : ℕ
hi : ∀ (m : ℕ), m < n → 1 < m → coeff (cyclotomic m R) 0 = 1
hn : 1 < n
hleq : ∀ (j : ℕ), j ∈ Finset.erase (Nat.properDivisors n) 1 → 2 ≤ j
⊢ ∀ (j : ℕ), j ∈ Finset.erase (Nat.properDivisors n) 1 → coeff (cyclotomic j R) 0 = 1
[PROOFSTEP]
intro j hj
[GOAL]
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
hn✝ : 1 < n✝
n : ℕ
hi : ∀ (m : ℕ), m < n → 1 < m → coeff (cyclotomic m R) 0 = 1
hn : 1 < n
hleq : ∀ (j : ℕ), j ∈ Finset.erase (Nat.properDivisors n) 1 → 2 ≤ j
j : ℕ
hj : j ∈ Finset.erase (Nat.properDivisors n) 1
⊢ coeff (cyclotomic j R) 0 = 1
[PROOFSTEP]
exact hi j (Nat.mem_properDivisors.1 (Finset.mem_erase.1 hj).2).2 (hleq j hj)
[GOAL]
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
hn✝ : 1 < n✝
n : ℕ
hi : ∀ (m : ℕ), m < n → 1 < m → coeff (cyclotomic m R) 0 = 1
hn : 1 < n
hleq : ∀ (j : ℕ), j ∈ Finset.erase (Nat.properDivisors n) 1 → 2 ≤ j
hcongr : ∀ (j : ℕ), j ∈ Finset.erase (Nat.properDivisors n) 1 → coeff (cyclotomic j R) 0 = 1
⊢ coeff (X - 1) 0 * ∏ x in Finset.erase (Nat.properDivisors n) 1, coeff (cyclotomic x R) 0 = -1
[PROOFSTEP]
have hrw : (∏ x : ℕ in n.properDivisors.erase 1, (cyclotomic x R).coeff 0) = 1 :=
  by
  rw [Finset.prod_congr (refl (n.properDivisors.erase 1)) hcongr]
  simp only [Finset.prod_const_one]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
hn✝ : 1 < n✝
n : ℕ
hi : ∀ (m : ℕ), m < n → 1 < m → coeff (cyclotomic m R) 0 = 1
hn : 1 < n
hleq : ∀ (j : ℕ), j ∈ Finset.erase (Nat.properDivisors n) 1 → 2 ≤ j
hcongr : ∀ (j : ℕ), j ∈ Finset.erase (Nat.properDivisors n) 1 → coeff (cyclotomic j R) 0 = 1
⊢ ∏ x in Finset.erase (Nat.properDivisors n) 1, coeff (cyclotomic x R) 0 = 1
[PROOFSTEP]
rw [Finset.prod_congr (refl (n.properDivisors.erase 1)) hcongr]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
hn✝ : 1 < n✝
n : ℕ
hi : ∀ (m : ℕ), m < n → 1 < m → coeff (cyclotomic m R) 0 = 1
hn : 1 < n
hleq : ∀ (j : ℕ), j ∈ Finset.erase (Nat.properDivisors n) 1 → 2 ≤ j
hcongr : ∀ (j : ℕ), j ∈ Finset.erase (Nat.properDivisors n) 1 → coeff (cyclotomic j R) 0 = 1
⊢ ∏ x in Finset.erase (Nat.properDivisors n) 1, 1 = 1
[PROOFSTEP]
simp only [Finset.prod_const_one]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
hn✝ : 1 < n✝
n : ℕ
hi : ∀ (m : ℕ), m < n → 1 < m → coeff (cyclotomic m R) 0 = 1
hn : 1 < n
hleq : ∀ (j : ℕ), j ∈ Finset.erase (Nat.properDivisors n) 1 → 2 ≤ j
hcongr : ∀ (j : ℕ), j ∈ Finset.erase (Nat.properDivisors n) 1 → coeff (cyclotomic j R) 0 = 1
hrw : ∏ x in Finset.erase (Nat.properDivisors n) 1, coeff (cyclotomic x R) 0 = 1
⊢ coeff (X - 1) 0 * ∏ x in Finset.erase (Nat.properDivisors n) 1, coeff (cyclotomic x R) 0 = -1
[PROOFSTEP]
simp only [hrw, mul_one, zero_sub, coeff_one_zero, coeff_X_zero, coeff_sub]
[GOAL]
case h
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
hn✝ : 1 < n✝
n : ℕ
hi : ∀ (m : ℕ), m < n → 1 < m → coeff (cyclotomic m R) 0 = 1
hn : 1 < n
hprod : ∏ i in Nat.properDivisors n, coeff (cyclotomic i R) 0 = -1
⊢ coeff (cyclotomic n R) 0 = 1
[PROOFSTEP]
have heq : (X ^ n - 1 : R[X]).coeff 0 = -(cyclotomic n R).coeff 0 := by
  rw [← prod_cyclotomic_eq_X_pow_sub_one (zero_le_one.trans_lt hn), ← Nat.cons_self_properDivisors hn.ne_bot,
    Finset.prod_cons, mul_coeff_zero, coeff_zero_prod, hprod, mul_neg, mul_one]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
hn✝ : 1 < n✝
n : ℕ
hi : ∀ (m : ℕ), m < n → 1 < m → coeff (cyclotomic m R) 0 = 1
hn : 1 < n
hprod : ∏ i in Nat.properDivisors n, coeff (cyclotomic i R) 0 = -1
⊢ coeff (X ^ n - 1) 0 = -coeff (cyclotomic n R) 0
[PROOFSTEP]
rw [← prod_cyclotomic_eq_X_pow_sub_one (zero_le_one.trans_lt hn), ← Nat.cons_self_properDivisors hn.ne_bot,
  Finset.prod_cons, mul_coeff_zero, coeff_zero_prod, hprod, mul_neg, mul_one]
[GOAL]
case h
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
hn✝ : 1 < n✝
n : ℕ
hi : ∀ (m : ℕ), m < n → 1 < m → coeff (cyclotomic m R) 0 = 1
hn : 1 < n
hprod : ∏ i in Nat.properDivisors n, coeff (cyclotomic i R) 0 = -1
heq : coeff (X ^ n - 1) 0 = -coeff (cyclotomic n R) 0
⊢ coeff (cyclotomic n R) 0 = 1
[PROOFSTEP]
have hzero : (X ^ n - 1 : R[X]).coeff 0 = (-1 : R) :=
  by
  rw [coeff_zero_eq_eval_zero _]
  simp only [zero_pow (lt_of_lt_of_le zero_lt_two hn), eval_X, eval_one, zero_sub, eval_pow, eval_sub]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
hn✝ : 1 < n✝
n : ℕ
hi : ∀ (m : ℕ), m < n → 1 < m → coeff (cyclotomic m R) 0 = 1
hn : 1 < n
hprod : ∏ i in Nat.properDivisors n, coeff (cyclotomic i R) 0 = -1
heq : coeff (X ^ n - 1) 0 = -coeff (cyclotomic n R) 0
⊢ coeff (X ^ n - 1) 0 = -1
[PROOFSTEP]
rw [coeff_zero_eq_eval_zero _]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
hn✝ : 1 < n✝
n : ℕ
hi : ∀ (m : ℕ), m < n → 1 < m → coeff (cyclotomic m R) 0 = 1
hn : 1 < n
hprod : ∏ i in Nat.properDivisors n, coeff (cyclotomic i R) 0 = -1
heq : coeff (X ^ n - 1) 0 = -coeff (cyclotomic n R) 0
⊢ eval 0 (X ^ n - 1) = -1
[PROOFSTEP]
simp only [zero_pow (lt_of_lt_of_le zero_lt_two hn), eval_X, eval_one, zero_sub, eval_pow, eval_sub]
[GOAL]
case h
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
hn✝ : 1 < n✝
n : ℕ
hi : ∀ (m : ℕ), m < n → 1 < m → coeff (cyclotomic m R) 0 = 1
hn : 1 < n
hprod : ∏ i in Nat.properDivisors n, coeff (cyclotomic i R) 0 = -1
heq : coeff (X ^ n - 1) 0 = -coeff (cyclotomic n R) 0
hzero : coeff (X ^ n - 1) 0 = -1
⊢ coeff (cyclotomic n R) 0 = 1
[PROOFSTEP]
rw [hzero] at heq
[GOAL]
case h
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
hn✝ : 1 < n✝
n : ℕ
hi : ∀ (m : ℕ), m < n → 1 < m → coeff (cyclotomic m R) 0 = 1
hn : 1 < n
hprod : ∏ i in Nat.properDivisors n, coeff (cyclotomic i R) 0 = -1
heq : -1 = -coeff (cyclotomic n R) 0
hzero : coeff (X ^ n - 1) 0 = -1
⊢ coeff (cyclotomic n R) 0 = 1
[PROOFSTEP]
exact neg_inj.mp (Eq.symm heq)
[GOAL]
n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot : IsRoot (cyclotomic n (ZMod p)) (↑(Nat.castRingHom (ZMod p)) a)
⊢ Nat.coprime a p
[PROOFSTEP]
apply Nat.coprime.symm
[GOAL]
case a
n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot : IsRoot (cyclotomic n (ZMod p)) (↑(Nat.castRingHom (ZMod p)) a)
⊢ Nat.coprime p a
[PROOFSTEP]
rw [hprime.1.coprime_iff_not_dvd]
[GOAL]
case a
n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot : IsRoot (cyclotomic n (ZMod p)) (↑(Nat.castRingHom (ZMod p)) a)
⊢ ¬p ∣ a
[PROOFSTEP]
intro h
[GOAL]
case a
n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot : IsRoot (cyclotomic n (ZMod p)) (↑(Nat.castRingHom (ZMod p)) a)
h : p ∣ a
⊢ False
[PROOFSTEP]
replace h := (ZMod.nat_cast_zmod_eq_zero_iff_dvd a p).2 h
[GOAL]
case a
n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot : IsRoot (cyclotomic n (ZMod p)) (↑(Nat.castRingHom (ZMod p)) a)
h : ↑a = 0
⊢ False
[PROOFSTEP]
rw [IsRoot.def, eq_natCast, h, ← coeff_zero_eq_eval_zero] at hroot
[GOAL]
case a
n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot : coeff (cyclotomic n (ZMod p)) 0 = 0
h : ↑a = 0
⊢ False
[PROOFSTEP]
by_cases hone : n = 1
[GOAL]
case pos
n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot : coeff (cyclotomic n (ZMod p)) 0 = 0
h : ↑a = 0
hone : n = 1
⊢ False
[PROOFSTEP]
simp only [hone, cyclotomic_one, zero_sub, coeff_one_zero, coeff_X_zero, neg_eq_zero, one_ne_zero, coeff_sub] at hroot
[GOAL]
case neg
n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot : coeff (cyclotomic n (ZMod p)) 0 = 0
h : ↑a = 0
hone : ¬n = 1
⊢ False
[PROOFSTEP]
rw [cyclotomic_coeff_zero (ZMod p) (Nat.succ_le_of_lt (lt_of_le_of_ne (Nat.succ_le_of_lt hpos) (Ne.symm hone)))] at
  hroot
[GOAL]
case neg
n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot : 1 = 0
h : ↑a = 0
hone : ¬n = 1
⊢ False
[PROOFSTEP]
exact one_ne_zero hroot
[GOAL]
n : ℕ
hpos : 0 < n
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
hroot : IsRoot (cyclotomic n (ZMod p)) (↑(Nat.castRingHom (ZMod p)) a)
⊢ orderOf (ZMod.unitOfCoprime a (_ : Nat.coprime a p)) ∣ n
[PROOFSTEP]
apply orderOf_dvd_of_pow_eq_one
[GOAL]
case h
n : ℕ
hpos : 0 < n
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
hroot : IsRoot (cyclotomic n (ZMod p)) (↑(Nat.castRingHom (ZMod p)) a)
⊢ ZMod.unitOfCoprime a (_ : Nat.coprime a p) ^ n = 1
[PROOFSTEP]
suffices hpow : eval (Nat.castRingHom (ZMod p) a) (X ^ n - 1 : (ZMod p)[X]) = 0
[GOAL]
case h
n : ℕ
hpos : 0 < n
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
hroot : IsRoot (cyclotomic n (ZMod p)) (↑(Nat.castRingHom (ZMod p)) a)
hpow : eval (↑(Nat.castRingHom (ZMod p)) a) (X ^ n - 1) = 0
⊢ ZMod.unitOfCoprime a (_ : Nat.coprime a p) ^ n = 1
[PROOFSTEP]
simp only [eval_X, eval_one, eval_pow, eval_sub, eq_natCast] at hpow
[GOAL]
case h
n : ℕ
hpos : 0 < n
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
hroot : IsRoot (cyclotomic n (ZMod p)) (↑(Nat.castRingHom (ZMod p)) a)
hpow : ↑a ^ n - 1 = 0
⊢ ZMod.unitOfCoprime a (_ : Nat.coprime a p) ^ n = 1
[PROOFSTEP]
apply Units.val_eq_one.1
[GOAL]
case h
n : ℕ
hpos : 0 < n
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
hroot : IsRoot (cyclotomic n (ZMod p)) (↑(Nat.castRingHom (ZMod p)) a)
hpow : ↑a ^ n - 1 = 0
⊢ ↑(ZMod.unitOfCoprime a (_ : Nat.coprime a p) ^ n) = 1
[PROOFSTEP]
simp only [sub_eq_zero.mp hpow, ZMod.coe_unitOfCoprime, Units.val_pow_eq_pow_val]
[GOAL]
case hpow
n : ℕ
hpos : 0 < n
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
hroot : IsRoot (cyclotomic n (ZMod p)) (↑(Nat.castRingHom (ZMod p)) a)
⊢ eval (↑(Nat.castRingHom (ZMod p)) a) (X ^ n - 1) = 0
[PROOFSTEP]
rw [IsRoot.def] at hroot
[GOAL]
case hpow
n : ℕ
hpos : 0 < n
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
hroot : eval (↑(Nat.castRingHom (ZMod p)) a) (cyclotomic n (ZMod p)) = 0
⊢ eval (↑(Nat.castRingHom (ZMod p)) a) (X ^ n - 1) = 0
[PROOFSTEP]
rw [← prod_cyclotomic_eq_X_pow_sub_one hpos (ZMod p), ← Nat.cons_self_properDivisors hpos.ne', Finset.prod_cons,
  eval_mul, hroot, zero_mul]


[GOAL]
A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝² : CommRing K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
hS : S ≤ A⁰
s : { x // x ∈ S }
⊢ IsUnit (↑(algebraMap A K) ↑s)
[PROOFSTEP]
apply IsLocalization.map_units K (⟨s.1, hS s.2⟩ : A⁰)
[GOAL]
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
hS : S ≤ A⁰
src✝ : B →+* K := IsLocalization.lift (_ : ∀ (s : { x // x ∈ S }), IsUnit (↑(algebraMap A K) ↑s))
a : A
⊢ OneHom.toFun
      (↑↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ : ∀ (x y : B), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) })
      (↑(algebraMap A B) a) =
    ↑(algebraMap A K) a
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
hS : S ≤ A⁰
x : K
⊢ x ∈ AlgHom.range (mapToFractionRing K S B hS) →
    ∃ a s hs, x = IsLocalization.mk' K a { val := s, property := (_ : s ∈ A⁰) }
[PROOFSTEP]
rintro ⟨x, rfl⟩
[GOAL]
case intro
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
hS : S ≤ A⁰
x : B
⊢ ∃ a s hs, ↑↑(mapToFractionRing K S B hS) x = IsLocalization.mk' K a { val := s, property := (_ : s ∈ A⁰) }
[PROOFSTEP]
obtain ⟨a, s, rfl⟩ := IsLocalization.mk'_surjective S x
[GOAL]
case intro.intro.intro
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
hS : S ≤ A⁰
a : A
s : { x // x ∈ S }
⊢ ∃ a_1 s_1 hs,
    ↑↑(mapToFractionRing K S B hS) (IsLocalization.mk' B a s) =
      IsLocalization.mk' K a_1 { val := s_1, property := (_ : s_1 ∈ A⁰) }
[PROOFSTEP]
use a, s, s.2
[GOAL]
case h
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
hS : S ≤ A⁰
a : A
s : { x // x ∈ S }
⊢ ↑↑(mapToFractionRing K S B hS) (IsLocalization.mk' B a s) =
    IsLocalization.mk' K a { val := ↑s, property := (_ : ↑s ∈ A⁰) }
[PROOFSTEP]
apply IsLocalization.lift_mk'
[GOAL]
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
hS : S ≤ A⁰
x : K
⊢ (∃ a s hs, x = IsLocalization.mk' K a { val := s, property := (_ : s ∈ A⁰) }) →
    x ∈ AlgHom.range (mapToFractionRing K S B hS)
[PROOFSTEP]
rintro ⟨a, s, hs, rfl⟩
[GOAL]
case intro.intro.intro
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
hS : S ≤ A⁰
a s : A
hs : s ∈ S
⊢ IsLocalization.mk' K a { val := s, property := (_ : s ∈ A⁰) } ∈ AlgHom.range (mapToFractionRing K S B hS)
[PROOFSTEP]
use IsLocalization.mk' _ a ⟨s, hs⟩
[GOAL]
case h
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
hS : S ≤ A⁰
a s : A
hs : s ∈ S
⊢ ↑↑(mapToFractionRing K S B hS) (IsLocalization.mk' B a { val := s, property := hs }) =
    IsLocalization.mk' K a { val := s, property := (_ : s ∈ A⁰) }
[PROOFSTEP]
apply IsLocalization.lift_mk'
[GOAL]
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
hS : S ≤ A⁰
⊢ Function.Bijective ↑(AlgHom.rangeRestrict (mapToFractionRing K S B hS))
[PROOFSTEP]
refine' ⟨fun a b h => _, Set.surjective_onto_range⟩
[GOAL]
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
hS : S ≤ A⁰
a b : B
h : ↑(AlgHom.rangeRestrict (mapToFractionRing K S B hS)) a = ↑(AlgHom.rangeRestrict (mapToFractionRing K S B hS)) b
⊢ a = b
[PROOFSTEP]
refine' (IsLocalization.lift_injective_iff _).2 (fun a b => _) (Subtype.ext_iff.1 h)
[GOAL]
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
hS : S ≤ A⁰
a✝ b✝ : B
h : ↑(AlgHom.rangeRestrict (mapToFractionRing K S B hS)) a✝ = ↑(AlgHom.rangeRestrict (mapToFractionRing K S B hS)) b✝
a b : A
⊢ ↑(algebraMap A B) a = ↑(algebraMap A B) b ↔ ↑(algebraMap A K) a = ↑(algebraMap A K) b
[PROOFSTEP]
exact ⟨fun h => congr_arg _ (IsLocalization.injective _ hS h), fun h => congr_arg _ (IsFractionRing.injective A K h)⟩
[GOAL]
A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝² : CommRing K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
hS : S ≤ A⁰
⊢ {x | ∃ a s hs, x = IsLocalization.mk' K a { val := s, property := (_ : s ∈ A⁰) }} =
    ↑(AlgHom.range (mapToFractionRing K S (Localization S) hS))
[PROOFSTEP]
ext
[GOAL]
case h
A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝² : CommRing K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
hS : S ≤ A⁰
x✝ : K
⊢ x✝ ∈ {x | ∃ a s hs, x = IsLocalization.mk' K a { val := s, property := (_ : s ∈ A⁰) }} ↔
    x✝ ∈ ↑(AlgHom.range (mapToFractionRing K S (Localization S) hS))
[PROOFSTEP]
symm
[GOAL]
case h
A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝² : CommRing K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
hS : S ≤ A⁰
x✝ : K
⊢ x✝ ∈ ↑(AlgHom.range (mapToFractionRing K S (Localization S) hS)) ↔
    x✝ ∈ {x | ∃ a s hs, x = IsLocalization.mk' K a { val := s, property := (_ : s ∈ A⁰) }}
[PROOFSTEP]
apply mem_range_mapToFractionRing_iff
[GOAL]
A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝² : CommRing K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
⊢ IsLocalization S { x // x ∈ subalgebra K S hS }
[PROOFSTEP]
dsimp only [Localization.subalgebra]
[GOAL]
A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝² : CommRing K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
⊢ IsLocalization S
    { x //
      x ∈
        Subalgebra.copy (AlgHom.range (mapToFractionRing K S (Localization S) hS))
          {x | ∃ a s hs, x = IsLocalization.mk' K a { val := s, property := (_ : s ∈ A⁰) }}
          (_ :
            {x | ∃ a s hs, x = IsLocalization.mk' K a { val := s, property := (_ : s ∈ A⁰) }} =
              ↑(AlgHom.range (mapToFractionRing K S (Localization S) hS))) }
[PROOFSTEP]
rw [Subalgebra.copy_eq]
[GOAL]
A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝² : CommRing K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
⊢ IsLocalization S { x // x ∈ AlgHom.range (mapToFractionRing K S (Localization S) hS) }
[PROOFSTEP]
infer_instance
[GOAL]
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝⁵ : Field K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
x : K
⊢ x ∈ AlgHom.range (mapToFractionRing K S B hS) ↔ ∃ a s x_1, x = ↑(algebraMap A K) a * (↑(algebraMap A K) s)⁻¹
[PROOFSTEP]
rw [mem_range_mapToFractionRing_iff]
[GOAL]
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝⁵ : Field K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
x : K
⊢ (∃ a s hs, x = IsLocalization.mk' K a { val := s, property := (_ : s ∈ A⁰) }) ↔
    ∃ a s x_1, x = ↑(algebraMap A K) a * (↑(algebraMap A K) s)⁻¹
[PROOFSTEP]
convert Iff.rfl
[GOAL]
case h.e'_2.h.e'_2.h.h.e'_2.h.h.e'_2.h.h.e'_3
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝⁵ : Field K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
x : K
x✝² x✝¹ : A
x✝ : x✝¹ ∈ S
⊢ ↑(algebraMap A K) x✝² * (↑(algebraMap A K) x✝¹)⁻¹ =
    IsLocalization.mk' K x✝² { val := x✝¹, property := (_ : x✝¹ ∈ A⁰) }
[PROOFSTEP]
congr
[GOAL]
case h.e'_2.h.e'_2.h.h.e'_2.h.h.e'_2.h.h.e'_3.e_a
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝⁵ : Field K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
x : K
x✝² x✝¹ : A
x✝ : x✝¹ ∈ S
⊢ (↑(algebraMap A K) x✝¹)⁻¹ =
    ↑(↑(IsUnit.liftRight
              (MonoidHom.restrict (Submonoid.LocalizationMap.toMap (IsLocalization.toLocalizationMap A⁰ K)) A⁰)
              (_ :
                ∀ (y : { x // x ∈ A⁰ }),
                  IsUnit (↑(Submonoid.LocalizationMap.toMap (IsLocalization.toLocalizationMap A⁰ K)) ↑y)))
          { val := x✝¹, property := (_ : x✝¹ ∈ A⁰) })⁻¹
[PROOFSTEP]
rw [Units.val_inv_eq_inv_val]
[GOAL]
case h.e'_2.h.e'_2.h.h.e'_2.h.h.e'_2.h.h.e'_3.e_a
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝⁵ : Field K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
x : K
x✝² x✝¹ : A
x✝ : x✝¹ ∈ S
⊢ (↑(algebraMap A K) x✝¹)⁻¹ =
    (↑(↑(IsUnit.liftRight
              (MonoidHom.restrict (Submonoid.LocalizationMap.toMap (IsLocalization.toLocalizationMap A⁰ K)) A⁰)
              (_ :
                ∀ (y : { x // x ∈ A⁰ }),
                  IsUnit (↑(Submonoid.LocalizationMap.toMap (IsLocalization.toLocalizationMap A⁰ K)) ↑y)))
          { val := x✝¹, property := (_ : x✝¹ ∈ A⁰) }))⁻¹
[PROOFSTEP]
rfl
[GOAL]
A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
⊢ {x | ∃ a s x_1, x = ↑(algebraMap A K) a * (↑(algebraMap A K) s)⁻¹} =
    ↑(AlgHom.range (mapToFractionRing K S (Localization S) hS))
[PROOFSTEP]
ext
[GOAL]
case h
A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x✝ : K
⊢ x✝ ∈ {x | ∃ a s x_1, x = ↑(algebraMap A K) a * (↑(algebraMap A K) s)⁻¹} ↔
    x✝ ∈ ↑(AlgHom.range (mapToFractionRing K S (Localization S) hS))
[PROOFSTEP]
symm
[GOAL]
case h
A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x✝ : K
⊢ x✝ ∈ ↑(AlgHom.range (mapToFractionRing K S (Localization S) hS)) ↔
    x✝ ∈ {x | ∃ a s x_1, x = ↑(algebraMap A K) a * (↑(algebraMap A K) s)⁻¹}
[PROOFSTEP]
apply mem_range_mapToFractionRing_iff_ofField
[GOAL]
A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
⊢ IsLocalization S { x // x ∈ ofField K S hS }
[PROOFSTEP]
dsimp only [Localization.subalgebra.ofField]
[GOAL]
A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
⊢ IsLocalization S
    { x //
      x ∈
        Subalgebra.copy (AlgHom.range (mapToFractionRing K S (Localization S) hS))
          {x | ∃ a s x_1, x = ↑(algebraMap A K) a * (↑(algebraMap A K) s)⁻¹}
          (_ :
            {x | ∃ a s x_1, x = ↑(algebraMap A K) a * (↑(algebraMap A K) s)⁻¹} =
              ↑(AlgHom.range (mapToFractionRing K S (Localization S) hS))) }
[PROOFSTEP]
rw [Subalgebra.copy_eq]
[GOAL]
A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
⊢ IsLocalization S { x // x ∈ AlgHom.range (mapToFractionRing K S (Localization S) hS) }
[PROOFSTEP]
infer_instance