-- Mathlib/RingTheory/RootsOfUnity/Minpoly.lean
theorem minpoly_dvd_expand {p : ℕ} (hdiv : ¬p ∣ n) :
    minpoly ℤ μ ∣ expand ℤ p (minpoly ℤ (μ ^ p))

Proof state:
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))

Tactic:
rcases n.eq_zero_or_pos with (rfl | hpos)

Result:
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))

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))

Proof state:
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))

Tactic:
refine minpoly.isIntegrallyClosed_dvd (h.isIntegral hpos) ?_

Result:
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

Proof state:
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

Tactic:
exact minpoly.aeval _ _

Result:
no goals

Proof state:
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))

Tactic:
letI : IsIntegrallyClosed ℤ := GCDMonoid.toIsIntegrallyClosed

Result:
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))

Proof state:
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

Tactic:
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]

Result:
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

Proof state:
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))

Tactic:
simp_all

Result:
no goals