[GOAL]
n : ℕ
K : Type u_1
inst✝ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
⊢ IsIntegral ℤ μ
[PROOFSTEP]
use X ^ n - 1
[GOAL]
case h
n : ℕ
K : Type u_1
inst✝ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
⊢ Monic (X ^ n - 1) ∧ eval₂ (algebraMap ℤ K) μ (X ^ n - 1) = 0
[PROOFSTEP]
constructor
[GOAL]
case h.left
n : ℕ
K : Type u_1
inst✝ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
⊢ Monic (X ^ n - 1)
[PROOFSTEP]
exact monic_X_pow_sub_C 1 (ne_of_lt hpos).symm
[GOAL]
case h.right
n : ℕ
K : Type u_1
inst✝ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
⊢ eval₂ (algebraMap ℤ K) μ (X ^ n - 1) = 0
[PROOFSTEP]
simp only [((IsPrimitiveRoot.iff_def μ n).mp h).left, eval₂_one, eval₂_X_pow, eval₂_sub, sub_self]
[GOAL]
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
⊢ minpoly ℤ μ ∣ X ^ n - 1
[PROOFSTEP]
rcases n.eq_zero_or_pos with (rfl | h0)
[GOAL]
case inl
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
h : IsPrimitiveRoot μ 0
⊢ minpoly ℤ μ ∣ X ^ 0 - 1
[PROOFSTEP]
simp
[GOAL]
case inr
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
h0 : n > 0
⊢ minpoly ℤ μ ∣ X ^ n - 1
[PROOFSTEP]
apply minpoly.isIntegrallyClosed_dvd (isIntegral h h0)
[GOAL]
case inr
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
h0 : n > 0
⊢ ↑(Polynomial.aeval μ) (X ^ n - 1) = 0
[PROOFSTEP]
simp only [((IsPrimitiveRoot.iff_def μ n).mp h).left, aeval_X_pow, eq_intCast, Int.cast_one, aeval_one, AlgHom.map_sub,
  sub_self]
[GOAL]
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
p : ℕ
inst✝ : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
⊢ Separable (map (Int.castRingHom (ZMod p)) (minpoly ℤ μ))
[PROOFSTEP]
have hdvd : map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ X ^ n - 1 :=
  by
  convert RingHom.map_dvd (mapRingHom (Int.castRingHom (ZMod p))) (minpoly_dvd_x_pow_sub_one h)
  simp only [map_sub, map_pow, coe_mapRingHom, map_X, map_one]
[GOAL]
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
p : ℕ
inst✝ : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
⊢ map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ X ^ n - 1
[PROOFSTEP]
convert RingHom.map_dvd (mapRingHom (Int.castRingHom (ZMod p))) (minpoly_dvd_x_pow_sub_one h)
[GOAL]
case h.e'_4
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
p : ℕ
inst✝ : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
⊢ X ^ n - 1 = ↑(mapRingHom (Int.castRingHom (ZMod p))) (X ^ n - 1)
[PROOFSTEP]
simp only [map_sub, map_pow, coe_mapRingHom, map_X, map_one]
[GOAL]
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
p : ℕ
inst✝ : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hdvd : map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ X ^ n - 1
⊢ Separable (map (Int.castRingHom (ZMod p)) (minpoly ℤ μ))
[PROOFSTEP]
refine' Separable.of_dvd (separable_X_pow_sub_C 1 _ one_ne_zero) hdvd
[GOAL]
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
p : ℕ
inst✝ : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hdvd : map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ X ^ n - 1
⊢ ↑n ≠ 0
[PROOFSTEP]
by_contra hzero
[GOAL]
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
p : ℕ
inst✝ : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hdvd : map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ X ^ n - 1
hzero : ↑n = 0
⊢ False
[PROOFSTEP]
exact hdiv ((ZMod.nat_cast_zmod_eq_zero_iff_dvd n p).1 hzero)
[GOAL]
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hdiv : ¬p ∣ n
⊢ minpoly ℤ μ ∣ ↑(expand ℤ p) (minpoly ℤ (μ ^ p))
[PROOFSTEP]
rcases n.eq_zero_or_pos with (rfl | hpos)
[GOAL]
case inl
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
h : IsPrimitiveRoot μ 0
hdiv : ¬p ∣ 0
⊢ minpoly ℤ μ ∣ ↑(expand ℤ p) (minpoly ℤ (μ ^ p))
[PROOFSTEP]
simp_all
[GOAL]
case inr
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hdiv : ¬p ∣ n
hpos : n > 0
⊢ minpoly ℤ μ ∣ ↑(expand ℤ p) (minpoly ℤ (μ ^ p))
[PROOFSTEP]
letI : IsIntegrallyClosed ℤ := GCDMonoid.toIsIntegrallyClosed
[GOAL]
case inr
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hdiv : ¬p ∣ n
hpos : n > 0
this : IsIntegrallyClosed ℤ := GCDMonoid.toIsIntegrallyClosed
⊢ minpoly ℤ μ ∣ ↑(expand ℤ p) (minpoly ℤ (μ ^ p))
[PROOFSTEP]
refine' minpoly.isIntegrallyClosed_dvd (h.isIntegral hpos) _
[GOAL]
case inr
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hdiv : ¬p ∣ n
hpos : n > 0
this : IsIntegrallyClosed ℤ := GCDMonoid.toIsIntegrallyClosed
⊢ ↑(Polynomial.aeval μ) (↑(expand ℤ p) (minpoly ℤ (μ ^ p))) = 0
[PROOFSTEP]
rw [aeval_def, coe_expand, ← comp, eval₂_eq_eval_map, map_comp, Polynomial.map_pow, map_X, eval_comp, eval_pow, eval_X,
  ← eval₂_eq_eval_map, ← aeval_def]
[GOAL]
case inr
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hdiv : ¬p ∣ n
hpos : n > 0
this : IsIntegrallyClosed ℤ := GCDMonoid.toIsIntegrallyClosed
⊢ ↑(Polynomial.aeval (μ ^ p)) (minpoly ℤ (μ ^ p)) = 0
[PROOFSTEP]
exact minpoly.aeval _ _
[GOAL]
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
⊢ map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) ^ p
[PROOFSTEP]
set Q := minpoly ℤ (μ ^ p)
[GOAL]
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
Q : ℤ[X] := minpoly ℤ (μ ^ p)
⊢ map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ map (Int.castRingHom (ZMod p)) Q ^ p
[PROOFSTEP]
have hfrob : map (Int.castRingHom (ZMod p)) Q ^ p = map (Int.castRingHom (ZMod p)) (expand ℤ p Q) := by
  rw [← ZMod.expand_card, map_expand]
[GOAL]
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
Q : ℤ[X] := minpoly ℤ (μ ^ p)
⊢ map (Int.castRingHom (ZMod p)) Q ^ p = map (Int.castRingHom (ZMod p)) (↑(expand ℤ p) Q)
[PROOFSTEP]
rw [← ZMod.expand_card, map_expand]
[GOAL]
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hfrob : map (Int.castRingHom (ZMod p)) Q ^ p = map (Int.castRingHom (ZMod p)) (↑(expand ℤ p) Q)
⊢ map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ map (Int.castRingHom (ZMod p)) Q ^ p
[PROOFSTEP]
rw [hfrob]
[GOAL]
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hfrob : map (Int.castRingHom (ZMod p)) Q ^ p = map (Int.castRingHom (ZMod p)) (↑(expand ℤ p) Q)
⊢ map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ map (Int.castRingHom (ZMod p)) (↑(expand ℤ p) Q)
[PROOFSTEP]
apply RingHom.map_dvd (mapRingHom (Int.castRingHom (ZMod p)))
[GOAL]
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hfrob : map (Int.castRingHom (ZMod p)) Q ^ p = map (Int.castRingHom (ZMod p)) (↑(expand ℤ p) Q)
⊢ minpoly ℤ μ ∣ ↑(expand ℤ p) Q
[PROOFSTEP]
exact minpoly_dvd_expand h hdiv
[GOAL]
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
⊢ minpoly ℤ μ = minpoly ℤ (μ ^ p)
[PROOFSTEP]
classical
by_cases hn : n = 0
· simp_all
have hpos := Nat.pos_of_ne_zero hn
by_contra hdiff
set P := minpoly ℤ μ
set Q := minpoly ℤ (μ ^ p)
have Pmonic : P.Monic := minpoly.monic (h.isIntegral hpos)
have Qmonic : Q.Monic := minpoly.monic ((h.pow_of_prime hprime.1 hdiv).isIntegral hpos)
have Pirr : Irreducible P := minpoly.irreducible (h.isIntegral hpos)
have Qirr : Irreducible Q := minpoly.irreducible ((h.pow_of_prime hprime.1 hdiv).isIntegral hpos)
have PQprim : IsPrimitive (P * Q) := Pmonic.isPrimitive.mul Qmonic.isPrimitive
have prod : P * Q ∣ X ^ n - 1 :=
  by
  rw [IsPrimitive.Int.dvd_iff_map_cast_dvd_map_cast (P * Q) (X ^ n - 1) PQprim
      (monic_X_pow_sub_C (1 : ℤ) (ne_of_gt hpos)).isPrimitive,
    Polynomial.map_mul]
  refine' IsCoprime.mul_dvd _ _ _
  · have aux := IsPrimitive.Int.irreducible_iff_irreducible_map_cast Pmonic.isPrimitive
    refine' (dvd_or_coprime _ _ (aux.1 Pirr)).resolve_left _
    rw [map_dvd_map (Int.castRingHom ℚ) Int.cast_injective Pmonic]
    intro hdiv
    refine' hdiff (eq_of_monic_of_associated Pmonic Qmonic _)
    exact associated_of_dvd_dvd hdiv (Pirr.dvd_symm Qirr hdiv)
  · apply (map_dvd_map (Int.castRingHom ℚ) Int.cast_injective Pmonic).2
    exact minpoly_dvd_x_pow_sub_one h
  · apply (map_dvd_map (Int.castRingHom ℚ) Int.cast_injective Qmonic).2
    exact minpoly_dvd_x_pow_sub_one (pow_of_prime h hprime.1 hdiv)
replace prod := RingHom.map_dvd (mapRingHom (Int.castRingHom (ZMod p))) prod
rw [coe_mapRingHom, Polynomial.map_mul, Polynomial.map_sub, Polynomial.map_one, Polynomial.map_pow, map_X] at prod 
obtain ⟨R, hR⟩ := minpoly_dvd_mod_p h hdiv
rw [hR, ← mul_assoc, ← Polynomial.map_mul, ← sq, Polynomial.map_pow] at prod 
have habs : map (Int.castRingHom (ZMod p)) P ^ 2 ∣ map (Int.castRingHom (ZMod p)) P ^ 2 * R := by use R
replace habs :=
  lt_of_lt_of_le (PartENat.coe_lt_coe.2 one_lt_two) (multiplicity.le_multiplicity_of_pow_dvd (dvd_trans habs prod))
have hfree : Squarefree (X ^ n - 1 : (ZMod p)[X]) :=
  (separable_X_pow_sub_C 1 (fun h => hdiv <| (ZMod.nat_cast_zmod_eq_zero_iff_dvd n p).1 h) one_ne_zero).squarefree
cases' (multiplicity.squarefree_iff_multiplicity_le_one (X ^ n - 1)).1 hfree (map (Int.castRingHom (ZMod p)) P) with hle
  hunit
· rw [Nat.cast_one] at habs ; exact hle.not_lt habs
· replace hunit := degree_eq_zero_of_isUnit hunit
  rw [degree_map_eq_of_leadingCoeff_ne_zero (Int.castRingHom (ZMod p)) _] at hunit 
  · exact (minpoly.degree_pos (isIntegral h hpos)).ne' hunit
  simp only [Pmonic, eq_intCast, Monic.leadingCoeff, Int.cast_one, Ne.def, not_false_iff, one_ne_zero]
[GOAL]
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
⊢ minpoly ℤ μ = minpoly ℤ (μ ^ p)
[PROOFSTEP]
by_cases hn : n = 0
[GOAL]
case pos
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : n = 0
⊢ minpoly ℤ μ = minpoly ℤ (μ ^ p)
[PROOFSTEP]
simp_all
[GOAL]
case neg
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
⊢ minpoly ℤ μ = minpoly ℤ (μ ^ p)
[PROOFSTEP]
have hpos := Nat.pos_of_ne_zero hn
[GOAL]
case neg
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
⊢ minpoly ℤ μ = minpoly ℤ (μ ^ p)
[PROOFSTEP]
by_contra hdiff
[GOAL]
case neg
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
hdiff : ¬minpoly ℤ μ = minpoly ℤ (μ ^ p)
⊢ False
[PROOFSTEP]
set P := minpoly ℤ μ
[GOAL]
case neg
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
hdiff : ¬P = minpoly ℤ (μ ^ p)
⊢ False
[PROOFSTEP]
set Q := minpoly ℤ (μ ^ p)
[GOAL]
case neg
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
⊢ False
[PROOFSTEP]
have Pmonic : P.Monic := minpoly.monic (h.isIntegral hpos)
[GOAL]
case neg
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
⊢ False
[PROOFSTEP]
have Qmonic : Q.Monic := minpoly.monic ((h.pow_of_prime hprime.1 hdiv).isIntegral hpos)
[GOAL]
case neg
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
⊢ False
[PROOFSTEP]
have Pirr : Irreducible P := minpoly.irreducible (h.isIntegral hpos)
[GOAL]
case neg
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
⊢ False
[PROOFSTEP]
have Qirr : Irreducible Q := minpoly.irreducible ((h.pow_of_prime hprime.1 hdiv).isIntegral hpos)
[GOAL]
case neg
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
⊢ False
[PROOFSTEP]
have PQprim : IsPrimitive (P * Q) := Pmonic.isPrimitive.mul Qmonic.isPrimitive
[GOAL]
case neg
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
⊢ False
[PROOFSTEP]
have prod : P * Q ∣ X ^ n - 1 :=
  by
  rw [IsPrimitive.Int.dvd_iff_map_cast_dvd_map_cast (P * Q) (X ^ n - 1) PQprim
      (monic_X_pow_sub_C (1 : ℤ) (ne_of_gt hpos)).isPrimitive,
    Polynomial.map_mul]
  refine' IsCoprime.mul_dvd _ _ _
  · have aux := IsPrimitive.Int.irreducible_iff_irreducible_map_cast Pmonic.isPrimitive
    refine' (dvd_or_coprime _ _ (aux.1 Pirr)).resolve_left _
    rw [map_dvd_map (Int.castRingHom ℚ) Int.cast_injective Pmonic]
    intro hdiv
    refine' hdiff (eq_of_monic_of_associated Pmonic Qmonic _)
    exact associated_of_dvd_dvd hdiv (Pirr.dvd_symm Qirr hdiv)
  · apply (map_dvd_map (Int.castRingHom ℚ) Int.cast_injective Pmonic).2
    exact minpoly_dvd_x_pow_sub_one h
  · apply (map_dvd_map (Int.castRingHom ℚ) Int.cast_injective Qmonic).2
    exact minpoly_dvd_x_pow_sub_one (pow_of_prime h hprime.1 hdiv)
[GOAL]
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
⊢ P * Q ∣ X ^ n - 1
[PROOFSTEP]
rw [IsPrimitive.Int.dvd_iff_map_cast_dvd_map_cast (P * Q) (X ^ n - 1) PQprim
    (monic_X_pow_sub_C (1 : ℤ) (ne_of_gt hpos)).isPrimitive,
  Polynomial.map_mul]
[GOAL]
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
⊢ map (Int.castRingHom ℚ) P * map (Int.castRingHom ℚ) Q ∣ map (Int.castRingHom ℚ) (X ^ n - 1)
[PROOFSTEP]
refine' IsCoprime.mul_dvd _ _ _
[GOAL]
case refine'_1
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
⊢ IsCoprime (map (Int.castRingHom ℚ) P) (map (Int.castRingHom ℚ) Q)
[PROOFSTEP]
have aux := IsPrimitive.Int.irreducible_iff_irreducible_map_cast Pmonic.isPrimitive
[GOAL]
case refine'_1
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
aux : Irreducible P ↔ Irreducible (map (Int.castRingHom ℚ) P)
⊢ IsCoprime (map (Int.castRingHom ℚ) P) (map (Int.castRingHom ℚ) Q)
[PROOFSTEP]
refine' (dvd_or_coprime _ _ (aux.1 Pirr)).resolve_left _
[GOAL]
case refine'_1
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
aux : Irreducible P ↔ Irreducible (map (Int.castRingHom ℚ) P)
⊢ ¬map (Int.castRingHom ℚ) P ∣ map (Int.castRingHom ℚ) Q
[PROOFSTEP]
rw [map_dvd_map (Int.castRingHom ℚ) Int.cast_injective Pmonic]
[GOAL]
case refine'_1
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
aux : Irreducible P ↔ Irreducible (map (Int.castRingHom ℚ) P)
⊢ ¬P ∣ Q
[PROOFSTEP]
intro hdiv
[GOAL]
case refine'_1
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv✝ : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
aux : Irreducible P ↔ Irreducible (map (Int.castRingHom ℚ) P)
hdiv : P ∣ Q
⊢ False
[PROOFSTEP]
refine' hdiff (eq_of_monic_of_associated Pmonic Qmonic _)
[GOAL]
case refine'_1
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv✝ : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
aux : Irreducible P ↔ Irreducible (map (Int.castRingHom ℚ) P)
hdiv : P ∣ Q
⊢ Associated P Q
[PROOFSTEP]
exact associated_of_dvd_dvd hdiv (Pirr.dvd_symm Qirr hdiv)
[GOAL]
case refine'_2
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
⊢ map (Int.castRingHom ℚ) P ∣ map (Int.castRingHom ℚ) (X ^ n - 1)
[PROOFSTEP]
apply (map_dvd_map (Int.castRingHom ℚ) Int.cast_injective Pmonic).2
[GOAL]
case refine'_2
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
⊢ P ∣ X ^ n - 1
[PROOFSTEP]
exact minpoly_dvd_x_pow_sub_one h
[GOAL]
case refine'_3
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
⊢ map (Int.castRingHom ℚ) Q ∣ map (Int.castRingHom ℚ) (X ^ n - 1)
[PROOFSTEP]
apply (map_dvd_map (Int.castRingHom ℚ) Int.cast_injective Qmonic).2
[GOAL]
case refine'_3
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
⊢ Q ∣ X ^ n - 1
[PROOFSTEP]
exact minpoly_dvd_x_pow_sub_one (pow_of_prime h hprime.1 hdiv)
[GOAL]
case neg
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
prod : P * Q ∣ X ^ n - 1
⊢ False
[PROOFSTEP]
replace prod := RingHom.map_dvd (mapRingHom (Int.castRingHom (ZMod p))) prod
[GOAL]
case neg
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
prod : ↑(mapRingHom (Int.castRingHom (ZMod p))) (P * Q) ∣ ↑(mapRingHom (Int.castRingHom (ZMod p))) (X ^ n - 1)
⊢ False
[PROOFSTEP]
rw [coe_mapRingHom, Polynomial.map_mul, Polynomial.map_sub, Polynomial.map_one, Polynomial.map_pow, map_X] at prod 
[GOAL]
case neg
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
prod : map (Int.castRingHom (ZMod p)) P * map (Int.castRingHom (ZMod p)) Q ∣ X ^ n - 1
⊢ False
[PROOFSTEP]
obtain ⟨R, hR⟩ := minpoly_dvd_mod_p h hdiv
[GOAL]
case neg.intro
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
prod : map (Int.castRingHom (ZMod p)) P * map (Int.castRingHom (ZMod p)) Q ∣ X ^ n - 1
R : (ZMod p)[X]
hR : map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) = map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) * R
⊢ False
[PROOFSTEP]
rw [hR, ← mul_assoc, ← Polynomial.map_mul, ← sq, Polynomial.map_pow] at prod 
[GOAL]
case neg.intro
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
R : (ZMod p)[X]
prod : map (Int.castRingHom (ZMod p)) P ^ 2 * R ∣ X ^ n - 1
hR : map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) = map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) * R
⊢ False
[PROOFSTEP]
have habs : map (Int.castRingHom (ZMod p)) P ^ 2 ∣ map (Int.castRingHom (ZMod p)) P ^ 2 * R := by use R
[GOAL]
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
R : (ZMod p)[X]
prod : map (Int.castRingHom (ZMod p)) P ^ 2 * R ∣ X ^ n - 1
hR : map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) = map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) * R
⊢ map (Int.castRingHom (ZMod p)) P ^ 2 ∣ map (Int.castRingHom (ZMod p)) P ^ 2 * R
[PROOFSTEP]
use R
[GOAL]
case neg.intro
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
R : (ZMod p)[X]
prod : map (Int.castRingHom (ZMod p)) P ^ 2 * R ∣ X ^ n - 1
hR : map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) = map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) * R
habs : map (Int.castRingHom (ZMod p)) P ^ 2 ∣ map (Int.castRingHom (ZMod p)) P ^ 2 * R
⊢ False
[PROOFSTEP]
replace habs :=
  lt_of_lt_of_le (PartENat.coe_lt_coe.2 one_lt_two) (multiplicity.le_multiplicity_of_pow_dvd (dvd_trans habs prod))
[GOAL]
case neg.intro
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
R : (ZMod p)[X]
prod : map (Int.castRingHom (ZMod p)) P ^ 2 * R ∣ X ^ n - 1
hR : map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) = map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) * R
habs : ↑1 < multiplicity (map (Int.castRingHom (ZMod p)) P) (X ^ n - 1)
⊢ False
[PROOFSTEP]
have hfree : Squarefree (X ^ n - 1 : (ZMod p)[X]) :=
  (separable_X_pow_sub_C 1 (fun h => hdiv <| (ZMod.nat_cast_zmod_eq_zero_iff_dvd n p).1 h) one_ne_zero).squarefree
[GOAL]
case neg.intro
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
R : (ZMod p)[X]
prod : map (Int.castRingHom (ZMod p)) P ^ 2 * R ∣ X ^ n - 1
hR : map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) = map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) * R
habs : ↑1 < multiplicity (map (Int.castRingHom (ZMod p)) P) (X ^ n - 1)
hfree : Squarefree (X ^ n - 1)
⊢ False
[PROOFSTEP]
cases' (multiplicity.squarefree_iff_multiplicity_le_one (X ^ n - 1)).1 hfree (map (Int.castRingHom (ZMod p)) P) with hle
  hunit
[GOAL]
case neg.intro.inl
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
R : (ZMod p)[X]
prod : map (Int.castRingHom (ZMod p)) P ^ 2 * R ∣ X ^ n - 1
hR : map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) = map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) * R
habs : ↑1 < multiplicity (map (Int.castRingHom (ZMod p)) P) (X ^ n - 1)
hfree : Squarefree (X ^ n - 1)
hle : multiplicity (map (Int.castRingHom (ZMod p)) P) (X ^ n - 1) ≤ 1
⊢ False
[PROOFSTEP]
rw [Nat.cast_one] at habs 
[GOAL]
case neg.intro.inl
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
R : (ZMod p)[X]
prod : map (Int.castRingHom (ZMod p)) P ^ 2 * R ∣ X ^ n - 1
hR : map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) = map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) * R
habs : 1 < multiplicity (map (Int.castRingHom (ZMod p)) P) (X ^ n - 1)
hfree : Squarefree (X ^ n - 1)
hle : multiplicity (map (Int.castRingHom (ZMod p)) P) (X ^ n - 1) ≤ 1
⊢ False
[PROOFSTEP]
exact hle.not_lt habs
[GOAL]
case neg.intro.inr
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
R : (ZMod p)[X]
prod : map (Int.castRingHom (ZMod p)) P ^ 2 * R ∣ X ^ n - 1
hR : map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) = map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) * R
habs : ↑1 < multiplicity (map (Int.castRingHom (ZMod p)) P) (X ^ n - 1)
hfree : Squarefree (X ^ n - 1)
hunit : IsUnit (map (Int.castRingHom (ZMod p)) P)
⊢ False
[PROOFSTEP]
replace hunit := degree_eq_zero_of_isUnit hunit
[GOAL]
case neg.intro.inr
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
R : (ZMod p)[X]
prod : map (Int.castRingHom (ZMod p)) P ^ 2 * R ∣ X ^ n - 1
hR : map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) = map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) * R
habs : ↑1 < multiplicity (map (Int.castRingHom (ZMod p)) P) (X ^ n - 1)
hfree : Squarefree (X ^ n - 1)
hunit : degree (map (Int.castRingHom (ZMod p)) P) = 0
⊢ False
[PROOFSTEP]
rw [degree_map_eq_of_leadingCoeff_ne_zero (Int.castRingHom (ZMod p)) _] at hunit 
[GOAL]
case neg.intro.inr
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
R : (ZMod p)[X]
prod : map (Int.castRingHom (ZMod p)) P ^ 2 * R ∣ X ^ n - 1
hR : map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) = map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) * R
habs : ↑1 < multiplicity (map (Int.castRingHom (ZMod p)) P) (X ^ n - 1)
hfree : Squarefree (X ^ n - 1)
hunit : degree P = 0
⊢ False
[PROOFSTEP]
exact (minpoly.degree_pos (isIntegral h hpos)).ne' hunit
[GOAL]
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
R : (ZMod p)[X]
prod : map (Int.castRingHom (ZMod p)) P ^ 2 * R ∣ X ^ n - 1
hR : map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) = map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) * R
habs : ↑1 < multiplicity (map (Int.castRingHom (ZMod p)) P) (X ^ n - 1)
hfree : Squarefree (X ^ n - 1)
hunit : degree (map (Int.castRingHom (ZMod p)) P) = 0
⊢ ↑(Int.castRingHom (ZMod p)) (leadingCoeff P) ≠ 0
[PROOFSTEP]
simp only [Pmonic, eq_intCast, Monic.leadingCoeff, Int.cast_one, Ne.def, not_false_iff, one_ne_zero]
[GOAL]
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
m : ℕ
hcop : Nat.coprime m n
⊢ minpoly ℤ μ = minpoly ℤ (μ ^ m)
[PROOFSTEP]
revert n hcop
[GOAL]
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m : ℕ
⊢ ∀ {n : ℕ}, IsPrimitiveRoot μ n → Nat.coprime m n → minpoly ℤ μ = minpoly ℤ (μ ^ m)
[PROOFSTEP]
refine' UniqueFactorizationMonoid.induction_on_prime m _ _ _
[GOAL]
case refine'_1
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ : ℕ
⊢ IsPrimitiveRoot μ n✝ → Nat.coprime 0 n✝ → minpoly ℤ μ = minpoly ℤ (μ ^ 0)
[PROOFSTEP]
intro h hn
[GOAL]
case refine'_1
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ : ℕ
h : IsPrimitiveRoot μ n✝
hn : Nat.coprime 0 n✝
⊢ minpoly ℤ μ = minpoly ℤ (μ ^ 0)
[PROOFSTEP]
congr
[GOAL]
case refine'_1.e_x
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ : ℕ
h : IsPrimitiveRoot μ n✝
hn : Nat.coprime 0 n✝
⊢ μ = μ ^ 0
[PROOFSTEP]
simpa [(Nat.coprime_zero_left _).mp hn] using h
[GOAL]
case refine'_2
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ : ℕ
⊢ ∀ (x : ℕ), IsUnit x → IsPrimitiveRoot μ n✝ → Nat.coprime x n✝ → minpoly ℤ μ = minpoly ℤ (μ ^ x)
[PROOFSTEP]
intro u hunit _ _
[GOAL]
case refine'_2
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ u : ℕ
hunit : IsUnit u
h✝ : IsPrimitiveRoot μ n✝
hcop✝ : Nat.coprime u n✝
⊢ minpoly ℤ μ = minpoly ℤ (μ ^ u)
[PROOFSTEP]
congr
[GOAL]
case refine'_2.e_x
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ u : ℕ
hunit : IsUnit u
h✝ : IsPrimitiveRoot μ n✝
hcop✝ : Nat.coprime u n✝
⊢ μ = μ ^ u
[PROOFSTEP]
simp [Nat.isUnit_iff.mp hunit]
[GOAL]
case refine'_3
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ : ℕ
⊢ ∀ (a p : ℕ),
    a ≠ 0 →
      Prime p →
        (IsPrimitiveRoot μ n✝ → Nat.coprime a n✝ → minpoly ℤ μ = minpoly ℤ (μ ^ a)) →
          IsPrimitiveRoot μ n✝ → Nat.coprime (p * a) n✝ → minpoly ℤ μ = minpoly ℤ (μ ^ (p * a))
[PROOFSTEP]
intro a p _ hprime
[GOAL]
case refine'_3
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ a p : ℕ
a✝ : a ≠ 0
hprime : Prime p
⊢ (IsPrimitiveRoot μ n✝ → Nat.coprime a n✝ → minpoly ℤ μ = minpoly ℤ (μ ^ a)) →
    IsPrimitiveRoot μ n✝ → Nat.coprime (p * a) n✝ → minpoly ℤ μ = minpoly ℤ (μ ^ (p * a))
[PROOFSTEP]
intro hind h hcop
[GOAL]
case refine'_3
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ a p : ℕ
a✝ : a ≠ 0
hprime : Prime p
hind : IsPrimitiveRoot μ n✝ → Nat.coprime a n✝ → minpoly ℤ μ = minpoly ℤ (μ ^ a)
h : IsPrimitiveRoot μ n✝
hcop : Nat.coprime (p * a) n✝
⊢ minpoly ℤ μ = minpoly ℤ (μ ^ (p * a))
[PROOFSTEP]
rw [hind h (Nat.coprime.coprime_mul_left hcop)]
[GOAL]
case refine'_3
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ a p : ℕ
a✝ : a ≠ 0
hprime : Prime p
hind : IsPrimitiveRoot μ n✝ → Nat.coprime a n✝ → minpoly ℤ μ = minpoly ℤ (μ ^ a)
h : IsPrimitiveRoot μ n✝
hcop : Nat.coprime (p * a) n✝
⊢ minpoly ℤ (μ ^ a) = minpoly ℤ (μ ^ (p * a))
[PROOFSTEP]
clear hind
[GOAL]
case refine'_3
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ a p : ℕ
a✝ : a ≠ 0
hprime : Prime p
h : IsPrimitiveRoot μ n✝
hcop : Nat.coprime (p * a) n✝
⊢ minpoly ℤ (μ ^ a) = minpoly ℤ (μ ^ (p * a))
[PROOFSTEP]
replace hprime := hprime.nat_prime
[GOAL]
case refine'_3
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ a p : ℕ
a✝ : a ≠ 0
h : IsPrimitiveRoot μ n✝
hcop : Nat.coprime (p * a) n✝
hprime : Nat.Prime p
⊢ minpoly ℤ (μ ^ a) = minpoly ℤ (μ ^ (p * a))
[PROOFSTEP]
have hdiv := (Nat.Prime.coprime_iff_not_dvd hprime).1 (Nat.coprime.coprime_mul_right hcop)
[GOAL]
case refine'_3
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ a p : ℕ
a✝ : a ≠ 0
h : IsPrimitiveRoot μ n✝
hcop : Nat.coprime (p * a) n✝
hprime : Nat.Prime p
hdiv : ¬p ∣ n✝
⊢ minpoly ℤ (μ ^ a) = minpoly ℤ (μ ^ (p * a))
[PROOFSTEP]
haveI := Fact.mk hprime
[GOAL]
case refine'_3
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ a p : ℕ
a✝ : a ≠ 0
h : IsPrimitiveRoot μ n✝
hcop : Nat.coprime (p * a) n✝
hprime : Nat.Prime p
hdiv : ¬p ∣ n✝
this : Fact (Nat.Prime p)
⊢ minpoly ℤ (μ ^ a) = minpoly ℤ (μ ^ (p * a))
[PROOFSTEP]
rw [minpoly_eq_pow (h.pow_of_coprime a (Nat.coprime.coprime_mul_left hcop)) hdiv]
[GOAL]
case refine'_3
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ a p : ℕ
a✝ : a ≠ 0
h : IsPrimitiveRoot μ n✝
hcop : Nat.coprime (p * a) n✝
hprime : Nat.Prime p
hdiv : ¬p ∣ n✝
this : Fact (Nat.Prime p)
⊢ minpoly ℤ ((μ ^ a) ^ p) = minpoly ℤ (μ ^ (p * a))
[PROOFSTEP]
congr 1
[GOAL]
case refine'_3.e_x
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ a p : ℕ
a✝ : a ≠ 0
h : IsPrimitiveRoot μ n✝
hcop : Nat.coprime (p * a) n✝
hprime : Nat.Prime p
hdiv : ¬p ∣ n✝
this : Fact (Nat.Prime p)
⊢ (μ ^ a) ^ p = μ ^ (p * a)
[PROOFSTEP]
ring
[GOAL]
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
m : ℕ
hcop : Nat.coprime m n
⊢ IsRoot (map (Int.castRingHom K) (minpoly ℤ μ)) (μ ^ m)
[PROOFSTEP]
simp only [minpoly_eq_pow_coprime h hcop, IsRoot.def, eval_map]
[GOAL]
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
m : ℕ
hcop : Nat.coprime m n
⊢ eval₂ (Int.castRingHom K) (μ ^ m) (minpoly ℤ (μ ^ m)) = 0
[PROOFSTEP]
exact minpoly.aeval ℤ (μ ^ m)
[GOAL]
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
⊢ primitiveRoots n K ⊆ Multiset.toFinset (roots (map (Int.castRingHom K) (minpoly ℤ μ)))
[PROOFSTEP]
by_cases hn : n = 0
[GOAL]
case pos
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
hn : n = 0
⊢ primitiveRoots n K ⊆ Multiset.toFinset (roots (map (Int.castRingHom K) (minpoly ℤ μ)))
[PROOFSTEP]
simp_all
[GOAL]
case neg
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
hn : ¬n = 0
⊢ primitiveRoots n K ⊆ Multiset.toFinset (roots (map (Int.castRingHom K) (minpoly ℤ μ)))
[PROOFSTEP]
have hpos := Nat.pos_of_ne_zero hn
[GOAL]
case neg
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
hn : ¬n = 0
hpos : 0 < n
⊢ primitiveRoots n K ⊆ Multiset.toFinset (roots (map (Int.castRingHom K) (minpoly ℤ μ)))
[PROOFSTEP]
intro x hx
[GOAL]
case neg
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
hn : ¬n = 0
hpos : 0 < n
x : K
hx : x ∈ primitiveRoots n K
⊢ x ∈ Multiset.toFinset (roots (map (Int.castRingHom K) (minpoly ℤ μ)))
[PROOFSTEP]
obtain ⟨m, _, hcop, rfl⟩ := (isPrimitiveRoot_iff h hpos).1 ((mem_primitiveRoots hpos).1 hx)
[GOAL]
case neg.intro.intro.intro
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
hn : ¬n = 0
hpos : 0 < n
m : ℕ
left✝ : m < n
hcop : Nat.coprime m n
hx : μ ^ m ∈ primitiveRoots n K
⊢ μ ^ m ∈ Multiset.toFinset (roots (map (Int.castRingHom K) (minpoly ℤ μ)))
[PROOFSTEP]
simp only [Multiset.mem_toFinset, mem_roots]
[GOAL]
case neg.intro.intro.intro
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
hn : ¬n = 0
hpos : 0 < n
m : ℕ
left✝ : m < n
hcop : Nat.coprime m n
hx : μ ^ m ∈ primitiveRoots n K
⊢ μ ^ m ∈ roots (map (Int.castRingHom K) (minpoly ℤ μ))
[PROOFSTEP]
convert pow_isRoot_minpoly h hcop
[GOAL]
case a
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
hn : ¬n = 0
hpos : 0 < n
m : ℕ
left✝ : m < n
hcop : Nat.coprime m n
hx : μ ^ m ∈ primitiveRoots n K
⊢ μ ^ m ∈ roots (map (Int.castRingHom K) (minpoly ℤ μ)) ↔ IsRoot (map (Int.castRingHom K) (minpoly ℤ μ)) (μ ^ m)
[PROOFSTEP]
rw [← mem_roots]
[GOAL]
case a
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
hn : ¬n = 0
hpos : 0 < n
m : ℕ
left✝ : m < n
hcop : Nat.coprime m n
hx : μ ^ m ∈ primitiveRoots n K
⊢ map (Int.castRingHom K) (minpoly ℤ μ) ≠ 0
[PROOFSTEP]
exact map_monic_ne_zero <| minpoly.monic <| isIntegral h hpos
[GOAL]
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
⊢ Nat.totient n ≤ natDegree (minpoly ℤ μ)
[PROOFSTEP]
classical
let P : ℤ[X] := minpoly ℤ μ
let P_K : K[X] := map (Int.castRingHom K) P
calc
  n.totient = (primitiveRoots n K).card := h.card_primitiveRoots.symm
  _ ≤ P_K.roots.toFinset.card := (Finset.card_le_of_subset (is_roots_of_minpoly h))
  _ ≤ Multiset.card P_K.roots := (Multiset.toFinset_card_le _)
  _ ≤ P_K.natDegree := (card_roots' _)
  _ ≤ P.natDegree := natDegree_map_le _ _
[GOAL]
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
⊢ Nat.totient n ≤ natDegree (minpoly ℤ μ)
[PROOFSTEP]
let P : ℤ[X] := minpoly ℤ μ
[GOAL]
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
P : ℤ[X] := minpoly ℤ μ
⊢ Nat.totient n ≤ natDegree (minpoly ℤ μ)
[PROOFSTEP]
let P_K : K[X] := map (Int.castRingHom K) P
[GOAL]
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
P : ℤ[X] := minpoly ℤ μ
P_K : K[X] := map (Int.castRingHom K) P
⊢ Nat.totient n ≤ natDegree (minpoly ℤ μ)
[PROOFSTEP]
calc
  n.totient = (primitiveRoots n K).card := h.card_primitiveRoots.symm
  _ ≤ P_K.roots.toFinset.card := (Finset.card_le_of_subset (is_roots_of_minpoly h))
  _ ≤ Multiset.card P_K.roots := (Multiset.toFinset_card_le _)
  _ ≤ P_K.natDegree := (card_roots' _)
  _ ≤ P.natDegree := natDegree_map_le _ _
