[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
ζ : R
i : ℕ
hi : i ∈ Nat.divisors n
h : IsRoot (cyclotomic i R) ζ
⊢ ζ ^ n = 1
[PROOFSTEP]
rcases n.eq_zero_or_pos with (rfl | hn)
[GOAL]
case inl
R : Type u_1
inst✝ : CommRing R
ζ : R
i : ℕ
h : IsRoot (cyclotomic i R) ζ
hi : i ∈ Nat.divisors 0
⊢ ζ ^ 0 = 1
[PROOFSTEP]
exact pow_zero _
[GOAL]
case inr
R : Type u_1
inst✝ : CommRing R
n : ℕ
ζ : R
i : ℕ
hi : i ∈ Nat.divisors n
h : IsRoot (cyclotomic i R) ζ
hn : n > 0
⊢ ζ ^ n = 1
[PROOFSTEP]
have := congr_arg (eval ζ) (prod_cyclotomic_eq_X_pow_sub_one hn R).symm
[GOAL]
case inr
R : Type u_1
inst✝ : CommRing R
n : ℕ
ζ : R
i : ℕ
hi : i ∈ Nat.divisors n
h : IsRoot (cyclotomic i R) ζ
hn : n > 0
this : eval ζ (X ^ n - 1) = eval ζ (∏ i in Nat.divisors n, cyclotomic i R)
⊢ ζ ^ n = 1
[PROOFSTEP]
rw [eval_sub, eval_pow, eval_X, eval_one] at this 
[GOAL]
case inr
R : Type u_1
inst✝ : CommRing R
n : ℕ
ζ : R
i : ℕ
hi : i ∈ Nat.divisors n
h : IsRoot (cyclotomic i R) ζ
hn : n > 0
this : ζ ^ n - 1 = eval ζ (∏ i in Nat.divisors n, cyclotomic i R)
⊢ ζ ^ n = 1
[PROOFSTEP]
convert eq_add_of_sub_eq' this
[GOAL]
case h.e'_3
R : Type u_1
inst✝ : CommRing R
n : ℕ
ζ : R
i : ℕ
hi : i ∈ Nat.divisors n
h : IsRoot (cyclotomic i R) ζ
hn : n > 0
this : ζ ^ n - 1 = eval ζ (∏ i in Nat.divisors n, cyclotomic i R)
⊢ 1 = 1 + eval ζ (∏ i in Nat.divisors n, cyclotomic i R)
[PROOFSTEP]
convert (add_zero (M := R) _).symm
[GOAL]
case h.e'_3.h.e'_6
R : Type u_1
inst✝ : CommRing R
n : ℕ
ζ : R
i : ℕ
hi : i ∈ Nat.divisors n
h : IsRoot (cyclotomic i R) ζ
hn : n > 0
this : ζ ^ n - 1 = eval ζ (∏ i in Nat.divisors n, cyclotomic i R)
⊢ eval ζ (∏ i in Nat.divisors n, cyclotomic i R) = 0
[PROOFSTEP]
apply eval_eq_zero_of_dvd_of_eval_eq_zero _ h
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
ζ : R
i : ℕ
hi : i ∈ Nat.divisors n
h : IsRoot (cyclotomic i R) ζ
hn : n > 0
this : ζ ^ n - 1 = eval ζ (∏ i in Nat.divisors n, cyclotomic i R)
⊢ cyclotomic i R ∣ ∏ i in Nat.divisors n, cyclotomic i R
[PROOFSTEP]
exact Finset.dvd_prod_of_mem _ hi
[GOAL]
R✝ : Type u_1
inst✝³ : CommRing R✝
n : ℕ
inst✝² : IsDomain R✝
h : 0 < n
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
⊢ ζ ^ n = 1 ↔ ∃ i, i ∈ Nat.divisors n ∧ IsRoot (cyclotomic i R) ζ
[PROOFSTEP]
rw [← mem_nthRoots h, nthRoots, mem_roots <| X_pow_sub_C_ne_zero h _, C_1, ← prod_cyclotomic_eq_X_pow_sub_one h,
  isRoot_prod]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : IsDomain R
hpos : 0 < n
μ : R
h : IsPrimitiveRoot μ n
⊢ IsRoot (cyclotomic n R) μ
[PROOFSTEP]
rw [← mem_roots (cyclotomic_ne_zero n R), cyclotomic_eq_prod_X_sub_primitiveRoots h, roots_prod_X_sub_C, ←
  Finset.mem_def]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : IsDomain R
hpos : 0 < n
μ : R
h : IsPrimitiveRoot μ n
⊢ μ ∈ primitiveRoots n R
[PROOFSTEP]
rwa [← mem_primitiveRoots hpos] at h 
[GOAL]
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
⊢ IsRoot (cyclotomic n K) μ ↔ IsPrimitiveRoot μ n
[PROOFSTEP]
have hnpos : 0 < n := (NeZero.of_neZero_natCast K).out.bot_lt
[GOAL]
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
⊢ IsRoot (cyclotomic n K) μ ↔ IsPrimitiveRoot μ n
[PROOFSTEP]
refine' ⟨fun hμ => _, IsPrimitiveRoot.isRoot_cyclotomic hnpos⟩
[GOAL]
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
⊢ IsPrimitiveRoot μ n
[PROOFSTEP]
have hμn : μ ^ n = 1 := by
  rw [isRoot_of_unity_iff hnpos _]
  exact ⟨n, n.mem_divisors_self hnpos.ne', hμ⟩
[GOAL]
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
⊢ μ ^ n = 1
[PROOFSTEP]
rw [isRoot_of_unity_iff hnpos _]
[GOAL]
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
⊢ ∃ i, i ∈ Nat.divisors n ∧ IsRoot (cyclotomic i K) μ
[PROOFSTEP]
exact ⟨n, n.mem_divisors_self hnpos.ne', hμ⟩
[GOAL]
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
hμn : μ ^ n = 1
⊢ IsPrimitiveRoot μ n
[PROOFSTEP]
by_contra hnμ
[GOAL]
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
hμn : μ ^ n = 1
hnμ : ¬IsPrimitiveRoot μ n
⊢ False
[PROOFSTEP]
have ho : 0 < orderOf μ := by
  apply orderOf_pos'
  rw [isOfFinOrder_iff_pow_eq_one]
  exact ⟨n, hnpos, hμn⟩
[GOAL]
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
hμn : μ ^ n = 1
hnμ : ¬IsPrimitiveRoot μ n
⊢ 0 < orderOf μ
[PROOFSTEP]
apply orderOf_pos'
[GOAL]
case h
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
hμn : μ ^ n = 1
hnμ : ¬IsPrimitiveRoot μ n
⊢ IsOfFinOrder μ
[PROOFSTEP]
rw [isOfFinOrder_iff_pow_eq_one]
[GOAL]
case h
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
hμn : μ ^ n = 1
hnμ : ¬IsPrimitiveRoot μ n
⊢ ∃ n, 0 < n ∧ μ ^ n = 1
[PROOFSTEP]
exact ⟨n, hnpos, hμn⟩
[GOAL]
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
hμn : μ ^ n = 1
hnμ : ¬IsPrimitiveRoot μ n
ho : 0 < orderOf μ
⊢ False
[PROOFSTEP]
have := pow_orderOf_eq_one μ
[GOAL]
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
hμn : μ ^ n = 1
hnμ : ¬IsPrimitiveRoot μ n
ho : 0 < orderOf μ
this : μ ^ orderOf μ = 1
⊢ False
[PROOFSTEP]
rw [isRoot_of_unity_iff ho] at this 
[GOAL]
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
hμn : μ ^ n = 1
hnμ : ¬IsPrimitiveRoot μ n
ho : 0 < orderOf μ
this : ∃ i, i ∈ Nat.divisors (orderOf μ) ∧ IsRoot (cyclotomic i K) μ
⊢ False
[PROOFSTEP]
obtain ⟨i, hio, hiμ⟩ := this
[GOAL]
case intro.intro
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
hμn : μ ^ n = 1
hnμ : ¬IsPrimitiveRoot μ n
ho : 0 < orderOf μ
i : ℕ
hio : i ∈ Nat.divisors (orderOf μ)
hiμ : IsRoot (cyclotomic i K) μ
⊢ False
[PROOFSTEP]
replace hio := Nat.dvd_of_mem_divisors hio
[GOAL]
case intro.intro
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
hμn : μ ^ n = 1
hnμ : ¬IsPrimitiveRoot μ n
ho : 0 < orderOf μ
i : ℕ
hiμ : IsRoot (cyclotomic i K) μ
hio : i ∣ orderOf μ
⊢ False
[PROOFSTEP]
rw [IsPrimitiveRoot.not_iff] at hnμ 
[GOAL]
case intro.intro
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
hμn : μ ^ n = 1
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hiμ : IsRoot (cyclotomic i K) μ
hio : i ∣ orderOf μ
⊢ False
[PROOFSTEP]
rw [← orderOf_dvd_iff_pow_eq_one] at hμn 
[GOAL]
case intro.intro
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hiμ : IsRoot (cyclotomic i K) μ
hio : i ∣ orderOf μ
⊢ False
[PROOFSTEP]
have key : i < n := (Nat.le_of_dvd ho hio).trans_lt ((Nat.le_of_dvd hnpos hμn).lt_of_ne hnμ)
[GOAL]
case intro.intro
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hiμ : IsRoot (cyclotomic i K) μ
hio : i ∣ orderOf μ
key : i < n
⊢ False
[PROOFSTEP]
have key' : i ∣ n := hio.trans hμn
[GOAL]
case intro.intro
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hiμ : IsRoot (cyclotomic i K) μ
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
⊢ False
[PROOFSTEP]
rw [← Polynomial.dvd_iff_isRoot] at hμ hiμ 
[GOAL]
case intro.intro
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : X - ↑C μ ∣ cyclotomic n K
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hiμ : X - ↑C μ ∣ cyclotomic i K
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
⊢ False
[PROOFSTEP]
have hni : { i, n } ⊆ n.divisors := by simpa [Finset.insert_subset_iff, key'] using hnpos.ne'
[GOAL]
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : X - ↑C μ ∣ cyclotomic n K
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hiμ : X - ↑C μ ∣ cyclotomic i K
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
⊢ {i, n} ⊆ Nat.divisors n
[PROOFSTEP]
simpa [Finset.insert_subset_iff, key'] using hnpos.ne'
[GOAL]
case intro.intro
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : X - ↑C μ ∣ cyclotomic n K
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hiμ : X - ↑C μ ∣ cyclotomic i K
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
hni : {i, n} ⊆ Nat.divisors n
⊢ False
[PROOFSTEP]
obtain ⟨k, hk⟩ := hiμ
[GOAL]
case intro.intro.intro
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : X - ↑C μ ∣ cyclotomic n K
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
hni : {i, n} ⊆ Nat.divisors n
k : K[X]
hk : cyclotomic i K = (X - ↑C μ) * k
⊢ False
[PROOFSTEP]
obtain ⟨j, hj⟩ := hμ
[GOAL]
case intro.intro.intro.intro
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
hni : {i, n} ⊆ Nat.divisors n
k : K[X]
hk : cyclotomic i K = (X - ↑C μ) * k
j : K[X]
hj : cyclotomic n K = (X - ↑C μ) * j
⊢ False
[PROOFSTEP]
have := prod_cyclotomic_eq_X_pow_sub_one hnpos K
[GOAL]
case intro.intro.intro.intro
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
hni : {i, n} ⊆ Nat.divisors n
k : K[X]
hk : cyclotomic i K = (X - ↑C μ) * k
j : K[X]
hj : cyclotomic n K = (X - ↑C μ) * j
this : ∏ i in Nat.divisors n, cyclotomic i K = X ^ n - 1
⊢ False
[PROOFSTEP]
rw [← Finset.prod_sdiff hni, Finset.prod_pair key.ne, hk, hj] at this 
[GOAL]
case intro.intro.intro.intro
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
hni : {i, n} ⊆ Nat.divisors n
k : K[X]
hk : cyclotomic i K = (X - ↑C μ) * k
j : K[X]
hj : cyclotomic n K = (X - ↑C μ) * j
this : (∏ x in Nat.divisors n \ {i, n}, cyclotomic x K) * ((X - ↑C μ) * k * ((X - ↑C μ) * j)) = X ^ n - 1
⊢ False
[PROOFSTEP]
have hn := (X_pow_sub_one_separable_iff.mpr <| NeZero.natCast_ne n K).squarefree
[GOAL]
case intro.intro.intro.intro
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
hni : {i, n} ⊆ Nat.divisors n
k : K[X]
hk : cyclotomic i K = (X - ↑C μ) * k
j : K[X]
hj : cyclotomic n K = (X - ↑C μ) * j
this : (∏ x in Nat.divisors n \ {i, n}, cyclotomic x K) * ((X - ↑C μ) * k * ((X - ↑C μ) * j)) = X ^ n - 1
hn : Squarefree (X ^ n - 1)
⊢ False
[PROOFSTEP]
rw [← this, Squarefree] at hn 
[GOAL]
case intro.intro.intro.intro
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
hni : {i, n} ⊆ Nat.divisors n
k : K[X]
hk : cyclotomic i K = (X - ↑C μ) * k
j : K[X]
hj : cyclotomic n K = (X - ↑C μ) * j
this : (∏ x in Nat.divisors n \ {i, n}, cyclotomic x K) * ((X - ↑C μ) * k * ((X - ↑C μ) * j)) = X ^ n - 1
hn :
  ∀ (x : K[X]),
    x * x ∣ (∏ x in Nat.divisors n \ {i, n}, cyclotomic x K) * ((X - ↑C μ) * k * ((X - ↑C μ) * j)) → IsUnit x
⊢ False
[PROOFSTEP]
contrapose! hn
[GOAL]
case intro.intro.intro.intro
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
hni : {i, n} ⊆ Nat.divisors n
k : K[X]
hk : cyclotomic i K = (X - ↑C μ) * k
j : K[X]
hj : cyclotomic n K = (X - ↑C μ) * j
this : (∏ x in Nat.divisors n \ {i, n}, cyclotomic x K) * ((X - ↑C μ) * k * ((X - ↑C μ) * j)) = X ^ n - 1
hn : ¬False
⊢ ∃ x, x * x ∣ (∏ x in Nat.divisors n \ {i, n}, cyclotomic x K) * ((X - ↑C μ) * k * ((X - ↑C μ) * j)) ∧ ¬IsUnit x
[PROOFSTEP]
refine' ⟨X - C μ, ⟨(∏ x in n.divisors \ { i, n }, cyclotomic x K) * k * j, by ring⟩, _⟩
[GOAL]
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
hni : {i, n} ⊆ Nat.divisors n
k : K[X]
hk : cyclotomic i K = (X - ↑C μ) * k
j : K[X]
hj : cyclotomic n K = (X - ↑C μ) * j
this : (∏ x in Nat.divisors n \ {i, n}, cyclotomic x K) * ((X - ↑C μ) * k * ((X - ↑C μ) * j)) = X ^ n - 1
hn : ¬False
⊢ (∏ x in Nat.divisors n \ {i, n}, cyclotomic x K) * ((X - ↑C μ) * k * ((X - ↑C μ) * j)) =
    (X - ↑C μ) * (X - ↑C μ) * ((∏ x in Nat.divisors n \ {i, n}, cyclotomic x K) * k * j)
[PROOFSTEP]
ring
[GOAL]
case intro.intro.intro.intro
R : Type u_1
inst✝³ : CommRing R
n✝ : ℕ
inst✝² : IsDomain R
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
hni : {i, n} ⊆ Nat.divisors n
k : K[X]
hk : cyclotomic i K = (X - ↑C μ) * k
j : K[X]
hj : cyclotomic n K = (X - ↑C μ) * j
this : (∏ x in Nat.divisors n \ {i, n}, cyclotomic x K) * ((X - ↑C μ) * k * ((X - ↑C μ) * j)) = X ^ n - 1
hn : ¬False
⊢ ¬IsUnit (X - ↑C μ)
[PROOFSTEP]
simp [Polynomial.isUnit_iff_degree_eq_zero]
[GOAL]
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
μ : R
⊢ IsRoot (cyclotomic n R) μ ↔ IsPrimitiveRoot μ n
[PROOFSTEP]
have hf : Function.Injective _ := IsFractionRing.injective R (FractionRing R)
[GOAL]
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
μ : R
hf : Function.Injective ↑(algebraMap R (FractionRing R))
⊢ IsRoot (cyclotomic n R) μ ↔ IsPrimitiveRoot μ n
[PROOFSTEP]
haveI : NeZero (n : FractionRing R) := NeZero.nat_of_injective hf
[GOAL]
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
μ : R
hf : Function.Injective ↑(algebraMap R (FractionRing R))
this : NeZero ↑n
⊢ IsRoot (cyclotomic n R) μ ↔ IsPrimitiveRoot μ n
[PROOFSTEP]
rw [← isRoot_map_iff hf, ← IsPrimitiveRoot.map_iff_of_injective hf, map_cyclotomic, ← isRoot_cyclotomic_iff']
[GOAL]
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
⊢ Multiset.Nodup (roots (cyclotomic n R))
[PROOFSTEP]
obtain h | ⟨ζ, hζ⟩ := (cyclotomic n R).roots.empty_or_exists_mem
[GOAL]
case inl
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
h : roots (cyclotomic n R) = 0
⊢ Multiset.Nodup (roots (cyclotomic n R))
[PROOFSTEP]
exact h.symm ▸ Multiset.nodup_zero
[GOAL]
case inr.intro
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
ζ : R
hζ : ζ ∈ roots (cyclotomic n R)
⊢ Multiset.Nodup (roots (cyclotomic n R))
[PROOFSTEP]
rw [mem_roots <| cyclotomic_ne_zero n R, isRoot_cyclotomic_iff] at hζ 
[GOAL]
case inr.intro
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
ζ : R
hζ : IsPrimitiveRoot ζ n
⊢ Multiset.Nodup (roots (cyclotomic n R))
[PROOFSTEP]
refine'
  Multiset.nodup_of_le
    (roots.le_of_dvd (X_pow_sub_C_ne_zero (NeZero.pos_of_neZero_natCast R) 1) <| cyclotomic.dvd_X_pow_sub_one n R)
    hζ.nthRoots_nodup
[GOAL]
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
⊢ { val := roots (cyclotomic n R), nodup := (_ : Multiset.Nodup (roots (cyclotomic n R))) } = primitiveRoots n R
[PROOFSTEP]
ext a
[GOAL]
case a
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
a : R
⊢ a ∈ { val := roots (cyclotomic n R), nodup := (_ : Multiset.Nodup (roots (cyclotomic n R))) } ↔ a ∈ primitiveRoots n R
[PROOFSTEP]
simp only [mem_primitiveRoots, NeZero.pos_of_neZero_natCast R]
[GOAL]
case a
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
a : R
⊢ a ∈ { val := roots (cyclotomic n R), nodup := (_ : Multiset.Nodup (roots (cyclotomic n R))) } ↔ IsPrimitiveRoot a n
[PROOFSTEP]
convert isRoot_cyclotomic_iff (n := n) (μ := a)
[GOAL]
case h.e'_1.a
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
a : R
⊢ a ∈ { val := roots (cyclotomic n R), nodup := (_ : Multiset.Nodup (roots (cyclotomic n R))) } ↔
    IsRoot (cyclotomic n R) a
[PROOFSTEP]
simp [cyclotomic_ne_zero n R]
[GOAL]
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
⊢ roots (cyclotomic n R) = (primitiveRoots n R).val
[PROOFSTEP]
rw [← cyclotomic.roots_to_finset_eq_primitiveRoots]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : CharZero R
⊢ Function.Injective fun n => cyclotomic n R
[PROOFSTEP]
intro n m hnm
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
n✝ : ℕ
inst✝ : CharZero R
n m : ℕ
hnm : (fun n => cyclotomic n R) n = (fun n => cyclotomic n R) m
⊢ n = m
[PROOFSTEP]
simp only at hnm 
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
n✝ : ℕ
inst✝ : CharZero R
n m : ℕ
hnm : cyclotomic n R = cyclotomic m R
⊢ n = m
[PROOFSTEP]
rcases eq_or_ne n 0 with (rfl | hzero)
[GOAL]
case inl
R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : CharZero R
m : ℕ
hnm : cyclotomic 0 R = cyclotomic m R
⊢ 0 = m
[PROOFSTEP]
rw [cyclotomic_zero] at hnm 
[GOAL]
case inl
R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : CharZero R
m : ℕ
hnm : 1 = cyclotomic m R
⊢ 0 = m
[PROOFSTEP]
replace hnm := congr_arg natDegree hnm
[GOAL]
case inl
R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : CharZero R
m : ℕ
hnm : natDegree 1 = natDegree (cyclotomic m R)
⊢ 0 = m
[PROOFSTEP]
rw [natDegree_one, natDegree_cyclotomic] at hnm 
[GOAL]
case inl
R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : CharZero R
m : ℕ
hnm : 0 = Nat.totient m
⊢ 0 = m
[PROOFSTEP]
by_contra h
[GOAL]
case inl
R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : CharZero R
m : ℕ
hnm : 0 = Nat.totient m
h : ¬0 = m
⊢ False
[PROOFSTEP]
exact (Nat.totient_pos (zero_lt_iff.2 (Ne.symm h))).ne hnm
[GOAL]
case inr
R : Type u_1
inst✝¹ : CommRing R
n✝ : ℕ
inst✝ : CharZero R
n m : ℕ
hnm : cyclotomic n R = cyclotomic m R
hzero : n ≠ 0
⊢ n = m
[PROOFSTEP]
haveI := NeZero.mk hzero
[GOAL]
case inr
R : Type u_1
inst✝¹ : CommRing R
n✝ : ℕ
inst✝ : CharZero R
n m : ℕ
hnm : cyclotomic n R = cyclotomic m R
hzero : n ≠ 0
this : NeZero n
⊢ n = m
[PROOFSTEP]
rw [← map_cyclotomic_int _ R, ← map_cyclotomic_int _ R] at hnm 
[GOAL]
case inr
R : Type u_1
inst✝¹ : CommRing R
n✝ : ℕ
inst✝ : CharZero R
n m : ℕ
hnm : map (Int.castRingHom R) (cyclotomic n ℤ) = map (Int.castRingHom R) (cyclotomic m ℤ)
hzero : n ≠ 0
this : NeZero n
⊢ n = m
[PROOFSTEP]
replace hnm := map_injective (Int.castRingHom R) Int.cast_injective hnm
[GOAL]
case inr
R : Type u_1
inst✝¹ : CommRing R
n✝ : ℕ
inst✝ : CharZero R
n m : ℕ
hzero : n ≠ 0
this : NeZero n
hnm : cyclotomic n ℤ = cyclotomic m ℤ
⊢ n = m
[PROOFSTEP]
replace hnm := congr_arg (map (Int.castRingHom ℂ)) hnm
[GOAL]
case inr
R : Type u_1
inst✝¹ : CommRing R
n✝ : ℕ
inst✝ : CharZero R
n m : ℕ
hzero : n ≠ 0
this : NeZero n
hnm : map (Int.castRingHom ℂ) (cyclotomic n ℤ) = map (Int.castRingHom ℂ) (cyclotomic m ℤ)
⊢ n = m
[PROOFSTEP]
rw [map_cyclotomic_int, map_cyclotomic_int] at hnm 
[GOAL]
case inr
R : Type u_1
inst✝¹ : CommRing R
n✝ : ℕ
inst✝ : CharZero R
n m : ℕ
hzero : n ≠ 0
this : NeZero n
hnm : cyclotomic n ℂ = cyclotomic m ℂ
⊢ n = m
[PROOFSTEP]
have hprim := Complex.isPrimitiveRoot_exp _ hzero
[GOAL]
case inr
R : Type u_1
inst✝¹ : CommRing R
n✝ : ℕ
inst✝ : CharZero R
n m : ℕ
hzero : n ≠ 0
this : NeZero n
hnm : cyclotomic n ℂ = cyclotomic m ℂ
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) n
⊢ n = m
[PROOFSTEP]
have hroot := isRoot_cyclotomic_iff (R := ℂ).2 hprim
[GOAL]
case inr
R : Type u_1
inst✝¹ : CommRing R
n✝ : ℕ
inst✝ : CharZero R
n m : ℕ
hzero : n ≠ 0
this : NeZero n
hnm : cyclotomic n ℂ = cyclotomic m ℂ
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) n
hroot : IsRoot (cyclotomic n ℂ) (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n))
⊢ n = m
[PROOFSTEP]
rw [hnm] at hroot 
[GOAL]
case inr
R : Type u_1
inst✝¹ : CommRing R
n✝ : ℕ
inst✝ : CharZero R
n m : ℕ
hzero : n ≠ 0
this : NeZero n
hnm : cyclotomic n ℂ = cyclotomic m ℂ
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) n
hroot : IsRoot (cyclotomic m ℂ) (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n))
⊢ n = m
[PROOFSTEP]
haveI hmzero : NeZero m := ⟨fun h => by simp [h] at hroot ⟩
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
n✝ : ℕ
inst✝ : CharZero R
n m : ℕ
hzero : n ≠ 0
this : NeZero n
hnm : cyclotomic n ℂ = cyclotomic m ℂ
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) n
hroot : IsRoot (cyclotomic m ℂ) (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n))
h : m = 0
⊢ False
[PROOFSTEP]
simp [h] at hroot 
[GOAL]
case inr
R : Type u_1
inst✝¹ : CommRing R
n✝ : ℕ
inst✝ : CharZero R
n m : ℕ
hzero : n ≠ 0
this : NeZero n
hnm : cyclotomic n ℂ = cyclotomic m ℂ
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) n
hroot : IsRoot (cyclotomic m ℂ) (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n))
hmzero : NeZero m
⊢ n = m
[PROOFSTEP]
rw [isRoot_cyclotomic_iff (R := ℂ)] at hroot 
[GOAL]
case inr
R : Type u_1
inst✝¹ : CommRing R
n✝ : ℕ
inst✝ : CharZero R
n m : ℕ
hzero : n ≠ 0
this : NeZero n
hnm : cyclotomic n ℂ = cyclotomic m ℂ
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) n
hroot : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) m
hmzero : NeZero m
⊢ n = m
[PROOFSTEP]
replace hprim := hprim.eq_orderOf
[GOAL]
case inr
R : Type u_1
inst✝¹ : CommRing R
n✝ : ℕ
inst✝ : CharZero R
n m : ℕ
hzero : n ≠ 0
this : NeZero n
hnm : cyclotomic n ℂ = cyclotomic m ℂ
hroot : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) m
hmzero : NeZero m
hprim : n = orderOf (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n))
⊢ n = m
[PROOFSTEP]
rwa [← IsPrimitiveRoot.eq_orderOf hroot] at hprim 
[GOAL]
R : Type u_1
inst✝² : CommRing R
n✝ n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
inst✝ : CharZero K
⊢ minpoly ℤ μ ∣ cyclotomic n ℤ
[PROOFSTEP]
apply minpoly.isIntegrallyClosed_dvd (h.isIntegral hpos)
[GOAL]
R : Type u_1
inst✝² : CommRing R
n✝ n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
inst✝ : CharZero K
⊢ ↑(aeval μ) (cyclotomic n ℤ) = 0
[PROOFSTEP]
simpa [aeval_def, eval₂_eq_eval_map, IsRoot.def] using h.isRoot_cyclotomic hpos
[GOAL]
R✝ : Type u_1
inst✝⁵ : CommRing R✝
n✝ : ℕ
K : Type u_2
inst✝⁴ : Field K
R : Type u_3
inst✝³ : CommRing R
inst✝² : IsDomain R
μ : R
n : ℕ
inst✝¹ : Algebra K R
hμ : IsPrimitiveRoot μ n
h : Irreducible (cyclotomic n K)
inst✝ : NeZero ↑n
⊢ cyclotomic n K = minpoly K μ
[PROOFSTEP]
haveI := NeZero.of_noZeroSMulDivisors K R n
[GOAL]
R✝ : Type u_1
inst✝⁵ : CommRing R✝
n✝ : ℕ
K : Type u_2
inst✝⁴ : Field K
R : Type u_3
inst✝³ : CommRing R
inst✝² : IsDomain R
μ : R
n : ℕ
inst✝¹ : Algebra K R
hμ : IsPrimitiveRoot μ n
h : Irreducible (cyclotomic n K)
inst✝ : NeZero ↑n
this : NeZero ↑n
⊢ cyclotomic n K = minpoly K μ
[PROOFSTEP]
refine' minpoly.eq_of_irreducible_of_monic h _ (cyclotomic.monic n K)
[GOAL]
R✝ : Type u_1
inst✝⁵ : CommRing R✝
n✝ : ℕ
K : Type u_2
inst✝⁴ : Field K
R : Type u_3
inst✝³ : CommRing R
inst✝² : IsDomain R
μ : R
n : ℕ
inst✝¹ : Algebra K R
hμ : IsPrimitiveRoot μ n
h : Irreducible (cyclotomic n K)
inst✝ : NeZero ↑n
this : NeZero ↑n
⊢ ↑(aeval μ) (cyclotomic n K) = 0
[PROOFSTEP]
rwa [aeval_def, eval₂_eq_eval_map, map_cyclotomic, ← IsRoot.def, isRoot_cyclotomic_iff]
[GOAL]
R : Type u_1
inst✝² : CommRing R
n✝ n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
inst✝ : CharZero K
⊢ cyclotomic n ℤ = minpoly ℤ μ
[PROOFSTEP]
refine'
  eq_of_monic_of_dvd_of_natDegree_le (minpoly.monic (IsPrimitiveRoot.isIntegral h hpos)) (cyclotomic.monic n ℤ)
    (h.minpoly_dvd_cyclotomic hpos) _
[GOAL]
R : Type u_1
inst✝² : CommRing R
n✝ n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
inst✝ : CharZero K
⊢ natDegree (cyclotomic n ℤ) ≤ natDegree (minpoly ℤ μ)
[PROOFSTEP]
simpa [natDegree_cyclotomic n ℤ] using totient_le_degree_minpoly h
[GOAL]
R : Type u_1
inst✝² : CommRing R
n✝ n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
inst✝ : CharZero K
⊢ cyclotomic n ℚ = minpoly ℚ μ
[PROOFSTEP]
rw [← map_cyclotomic_int, cyclotomic_eq_minpoly h hpos]
[GOAL]
R : Type u_1
inst✝² : CommRing R
n✝ n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
inst✝ : CharZero K
⊢ map (Int.castRingHom ℚ) (minpoly ℤ μ) = minpoly ℚ μ
[PROOFSTEP]
exact (minpoly.isIntegrallyClosed_eq_field_fractions' _ (IsPrimitiveRoot.isIntegral h hpos)).symm
[GOAL]
R : Type u_1
inst✝ : CommRing R
n✝ n : ℕ
hpos : 0 < n
⊢ Irreducible (cyclotomic n ℤ)
[PROOFSTEP]
rw [cyclotomic_eq_minpoly (isPrimitiveRoot_exp n hpos.ne') hpos]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n✝ n : ℕ
hpos : 0 < n
⊢ Irreducible (minpoly ℤ (exp (2 * ↑Real.pi * I / ↑n)))
[PROOFSTEP]
apply minpoly.irreducible
[GOAL]
case hx
R : Type u_1
inst✝ : CommRing R
n✝ n : ℕ
hpos : 0 < n
⊢ IsIntegral ℤ (exp (2 * ↑Real.pi * I / ↑n))
[PROOFSTEP]
exact (isPrimitiveRoot_exp n hpos.ne').isIntegral hpos
[GOAL]
R : Type u_1
inst✝ : CommRing R
n✝ n : ℕ
hpos : 0 < n
⊢ Irreducible (cyclotomic n ℚ)
[PROOFSTEP]
rw [← map_cyclotomic_int]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n✝ n : ℕ
hpos : 0 < n
⊢ Irreducible (map (Int.castRingHom ℚ) (cyclotomic n ℤ))
[PROOFSTEP]
exact
  (IsPrimitive.irreducible_iff_irreducible_map_fraction_map (cyclotomic.isPrimitive n ℤ)).1
    (cyclotomic.irreducible hpos)
[GOAL]
R : Type u_1
inst✝ : CommRing R
n✝ n m : ℕ
h : n ≠ m
⊢ IsCoprime (cyclotomic n ℚ) (cyclotomic m ℚ)
[PROOFSTEP]
rcases n.eq_zero_or_pos with (rfl | hnzero)
[GOAL]
case inl
R : Type u_1
inst✝ : CommRing R
n m : ℕ
h : 0 ≠ m
⊢ IsCoprime (cyclotomic 0 ℚ) (cyclotomic m ℚ)
[PROOFSTEP]
exact isCoprime_one_left
[GOAL]
case inr
R : Type u_1
inst✝ : CommRing R
n✝ n m : ℕ
h : n ≠ m
hnzero : n > 0
⊢ IsCoprime (cyclotomic n ℚ) (cyclotomic m ℚ)
[PROOFSTEP]
rcases m.eq_zero_or_pos with (rfl | hmzero)
[GOAL]
case inr.inl
R : Type u_1
inst✝ : CommRing R
n✝ n : ℕ
hnzero : n > 0
h : n ≠ 0
⊢ IsCoprime (cyclotomic n ℚ) (cyclotomic 0 ℚ)
[PROOFSTEP]
exact isCoprime_one_right
[GOAL]
case inr.inr
R : Type u_1
inst✝ : CommRing R
n✝ n m : ℕ
h : n ≠ m
hnzero : n > 0
hmzero : m > 0
⊢ IsCoprime (cyclotomic n ℚ) (cyclotomic m ℚ)
[PROOFSTEP]
rw [Irreducible.coprime_iff_not_dvd <| cyclotomic.irreducible_rat <| hnzero]
[GOAL]
case inr.inr
R : Type u_1
inst✝ : CommRing R
n✝ n m : ℕ
h : n ≠ m
hnzero : n > 0
hmzero : m > 0
⊢ ¬cyclotomic n ℚ ∣ cyclotomic m ℚ
[PROOFSTEP]
exact fun hdiv =>
  h <|
    cyclotomic_injective <|
      eq_of_monic_of_associated (cyclotomic.monic n ℚ) (cyclotomic.monic m ℚ) <|
        Irreducible.associated_of_dvd (cyclotomic.irreducible_rat hnzero) (cyclotomic.irreducible_rat hmzero) hdiv
