-- Mathlib/FieldTheory/Minpoly/Field.lean
/-- The minimal polynomial (over `K`) of `σ : Gal(L/K)` is `X ^ (orderOf σ) - 1`. -/
lemma minpoly_algEquiv_toLinearMap (σ : L ≃ₐ[K] L) (hσ : IsOfFinOrder σ) :
    minpoly K σ.toLinearMap = X ^ (orderOf σ) - C 1

Proof state:
case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
hσ : IsOfFinOrder σ
q : K[X]
hq : q.Monic
hs : (Polynomial.aeval σ.toLinearMap) q = 0
⊢ ¬q.natDegree < orderOf σ

Tactic:
intro H

Result:
case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
hσ : IsOfFinOrder σ
q : K[X]
hq : q.Monic
hs : (Polynomial.aeval σ.toLinearMap) q = 0
H : q.natDegree < orderOf σ
⊢ False

Proof state:
case refine_1
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
hσ : IsOfFinOrder σ
⊢ (Polynomial.aeval σ.toLinearMap) (X ^ orderOf σ - C 1) = 0

Tactic:
rw [map_sub]

Result:
case refine_1
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
hσ : IsOfFinOrder σ
⊢ (Polynomial.aeval σ.toLinearMap) (X ^ orderOf σ) - (Polynomial.aeval σ.toLinearMap) (C 1) = 0

Proof state:
case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
hσ : IsOfFinOrder σ
q : K[X]
hq : q.Monic
hs : (Polynomial.aeval σ.toLinearMap) q = 0
H : q.natDegree < orderOf σ
⊢ False

Tactic:
rw [aeval_eq_sum_range' H, ← Fin.sum_univ_eq_sum_range] at hs

Result:
case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
hσ : IsOfFinOrder σ
q : K[X]
hq : q.Monic
hs : ∑ i : Fin (orderOf σ), q.coeff ↑i • σ.toLinearMap ^ ↑i = 0
H : q.natDegree < orderOf σ
⊢ False

Proof state:
case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
hσ : IsOfFinOrder σ
q : K[X]
hq : q.Monic
H : q.natDegree < orderOf σ
hs : ∑ x : Fin (orderOf σ), q.coeff ↑x • (σ ^ ↑x).toLinearMap = 0
⊢ False

Tactic:
apply hq.ne_zero

Result:
case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
hσ : IsOfFinOrder σ
q : K[X]
hq : q.Monic
H : q.natDegree < orderOf σ
hs : ∑ x : Fin (orderOf σ), q.coeff ↑x • (σ ^ ↑x).toLinearMap = 0
⊢ q = 0

Proof state:
case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
hσ : IsOfFinOrder σ
⊢ ∀ (q : K[X]), q.Monic → (Polynomial.aeval σ.toLinearMap) q = 0 → (X ^ orderOf σ - C 1).degree ≤ q.degree

Tactic:
intros q hq hs

Result:
case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
hσ : IsOfFinOrder σ
q : K[X]
hq : q.Monic
hs : (Polynomial.aeval σ.toLinearMap) q = 0
⊢ (X ^ orderOf σ - C 1).degree ≤ q.degree

Proof state:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
hσ : IsOfFinOrder σ
⊢ minpoly K σ.toLinearMap = X ^ orderOf σ - C 1

Tactic:
refine (minpoly.unique _ _ (monic_X_pow_sub_C _ hσ.orderOf_pos.ne.symm) ?_ ?_).symm

Result:
case refine_1
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
hσ : IsOfFinOrder σ
⊢ (Polynomial.aeval σ.toLinearMap) (X ^ orderOf σ - C 1) = 0

case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
hσ : IsOfFinOrder σ
⊢ ∀ (q : K[X]), q.Monic → (Polynomial.aeval σ.toLinearMap) q = 0 → (X ^ orderOf σ - C 1).degree ≤ q.degree

Proof state:
case refine_1
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
hσ : IsOfFinOrder σ
⊢ (Polynomial.aeval σ.toLinearMap) (X ^ orderOf σ) - (Polynomial.aeval σ.toLinearMap) (C 1) = 0

Tactic:
simp [← AlgEquiv.pow_toLinearMap, pow_orderOf_eq_one]

Result:
no goals

Proof state:
case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
hσ : IsOfFinOrder σ
q : K[X]
hq : q.Monic
hs : ∑ i : Fin (orderOf σ), q.coeff ↑i • σ.toLinearMap ^ ↑i = 0
H : q.natDegree < orderOf σ
⊢ False

Tactic:
simp_rw [← AlgEquiv.pow_toLinearMap] at hs

Result:
case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
hσ : IsOfFinOrder σ
q : K[X]
hq : q.Monic
H : q.natDegree < orderOf σ
hs : ∑ x : Fin (orderOf σ), q.coeff ↑x • (σ ^ ↑x).toLinearMap = 0
⊢ False

Proof state:
case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
hσ : IsOfFinOrder σ
q : K[X]
hq : q.Monic
hs : (Polynomial.aeval σ.toLinearMap) q = 0
⊢ (X ^ orderOf σ - C 1).degree ≤ q.degree

Tactic:
rw [degree_eq_natDegree hq.ne_zero, degree_X_pow_sub_C hσ.orderOf_pos, Nat.cast_le, ← not_lt]

Result:
case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
hσ : IsOfFinOrder σ
q : K[X]
hq : q.Monic
hs : (Polynomial.aeval σ.toLinearMap) q = 0
⊢ ¬q.natDegree < orderOf σ

Proof state:
case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
hσ : IsOfFinOrder σ
q : K[X]
hq : q.Monic
H : q.natDegree < orderOf σ
hs : ∑ x : Fin (orderOf σ), q.coeff ↑x • (σ ^ ↑x).toLinearMap = 0
⊢ q = 0

Tactic:
simpa using Fintype.linearIndependent_iff.mp
  (((linearIndependent_algHom_toLinearMap' K L L).comp _ AlgEquiv.coe_algHom_injective).comp _
    (Subtype.val_injective.comp ((finEquivPowers σ hσ).injective)))
  (q.coeff ∘ (↑)) hs ⟨_, H⟩

Result:
no goals