[GOAL]
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
q : K[X]
hq : degree q = 1
⊢ eigenspace f (-coeff q 0 / leadingCoeff q) =
    LinearMap.ker (leadingCoeff q • f - ↑(algebraMap K (End K V)) (-coeff q 0))
[PROOFSTEP]
rw [eigenspace_div]
[GOAL]
case hb
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
q : K[X]
hq : degree q = 1
⊢ leadingCoeff q ≠ 0
[PROOFSTEP]
intro h
[GOAL]
case hb
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
q : K[X]
hq : degree q = 1
h : leadingCoeff q = 0
⊢ False
[PROOFSTEP]
rw [leadingCoeff_eq_zero_iff_deg_eq_bot.1 h] at hq 
[GOAL]
case hb
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
q : K[X]
hq : ⊥ = 1
h : leadingCoeff q = 0
⊢ False
[PROOFSTEP]
cases hq
[GOAL]
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
q : K[X]
hq : degree q = 1
⊢ LinearMap.ker (leadingCoeff q • f - ↑(algebraMap K (End K V)) (-coeff q 0)) =
    LinearMap.ker (↑(aeval f) (↑C (leadingCoeff q) * X + ↑C (coeff q 0)))
[PROOFSTEP]
rw [C_mul', aeval_def]
[GOAL]
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
q : K[X]
hq : degree q = 1
⊢ LinearMap.ker (leadingCoeff q • f - ↑(algebraMap K (End K V)) (-coeff q 0)) =
    LinearMap.ker (eval₂ (algebraMap K (End K V)) f (leadingCoeff q • X + ↑C (coeff q 0)))
[PROOFSTEP]
simp [algebraMap, Algebra.toRingHom]
[GOAL]
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
q : K[X]
hq : degree q = 1
⊢ LinearMap.ker (↑(aeval f) (↑C (leadingCoeff q) * X + ↑C (coeff q 0))) = LinearMap.ker (↑(aeval f) q)
[PROOFSTEP]
rwa [← eq_X_add_C_of_degree_eq_one]
[GOAL]
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
c : K[X]ˣ
⊢ LinearMap.ker (↑(aeval f) ↑c) = ⊥
[PROOFSTEP]
rw [Polynomial.eq_C_of_degree_eq_zero (degree_coe_units c)]
[GOAL]
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
c : K[X]ˣ
⊢ LinearMap.ker (↑(aeval f) (↑C (coeff (↑c) 0))) = ⊥
[PROOFSTEP]
simp only [aeval_def, eval₂_C]
[GOAL]
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
c : K[X]ˣ
⊢ LinearMap.ker (↑(algebraMap K (End K V)) (coeff (↑c) 0)) = ⊥
[PROOFSTEP]
apply ker_algebraMap_end
[GOAL]
case ha
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
c : K[X]ˣ
⊢ coeff (↑c) 0 ≠ 0
[PROOFSTEP]
apply coeff_coe_units_zero_ne_zero c
[GOAL]
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
p : K[X]
μ : K
x : V
h : HasEigenvector f μ x
⊢ ↑(↑(aeval f) p) x = eval μ p • x
[PROOFSTEP]
refine' p.induction_on _ _ _
[GOAL]
case refine'_1
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
p : K[X]
μ : K
x : V
h : HasEigenvector f μ x
⊢ ∀ (a : K), ↑(↑(aeval f) (↑C a)) x = eval μ (↑C a) • x
[PROOFSTEP]
intro a
[GOAL]
case refine'_1
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
p : K[X]
μ : K
x : V
h : HasEigenvector f μ x
a : K
⊢ ↑(↑(aeval f) (↑C a)) x = eval μ (↑C a) • x
[PROOFSTEP]
simp [Module.algebraMap_end_apply]
[GOAL]
case refine'_2
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
p : K[X]
μ : K
x : V
h : HasEigenvector f μ x
⊢ ∀ (p q : K[X]),
    ↑(↑(aeval f) p) x = eval μ p • x → ↑(↑(aeval f) q) x = eval μ q • x → ↑(↑(aeval f) (p + q)) x = eval μ (p + q) • x
[PROOFSTEP]
intro p q hp hq
[GOAL]
case refine'_2
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
p✝ : K[X]
μ : K
x : V
h : HasEigenvector f μ x
p q : K[X]
hp : ↑(↑(aeval f) p) x = eval μ p • x
hq : ↑(↑(aeval f) q) x = eval μ q • x
⊢ ↑(↑(aeval f) (p + q)) x = eval μ (p + q) • x
[PROOFSTEP]
simp [hp, hq, add_smul]
[GOAL]
case refine'_3
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
p : K[X]
μ : K
x : V
h : HasEigenvector f μ x
⊢ ∀ (n : ℕ) (a : K),
    ↑(↑(aeval f) (↑C a * X ^ n)) x = eval μ (↑C a * X ^ n) • x →
      ↑(↑(aeval f) (↑C a * X ^ (n + 1))) x = eval μ (↑C a * X ^ (n + 1)) • x
[PROOFSTEP]
intro n a hna
[GOAL]
case refine'_3
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
p : K[X]
μ : K
x : V
h : HasEigenvector f μ x
n : ℕ
a : K
hna : ↑(↑(aeval f) (↑C a * X ^ n)) x = eval μ (↑C a * X ^ n) • x
⊢ ↑(↑(aeval f) (↑C a * X ^ (n + 1))) x = eval μ (↑C a * X ^ (n + 1)) • x
[PROOFSTEP]
rw [mul_comm, pow_succ, mul_assoc, AlgHom.map_mul, LinearMap.mul_apply, mul_comm, hna]
[GOAL]
case refine'_3
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
p : K[X]
μ : K
x : V
h : HasEigenvector f μ x
n : ℕ
a : K
hna : ↑(↑(aeval f) (↑C a * X ^ n)) x = eval μ (↑C a * X ^ n) • x
⊢ ↑(↑(aeval f) X) (eval μ (↑C a * X ^ n) • x) = eval μ (X * (↑C a * X ^ n)) • x
[PROOFSTEP]
simp only [mem_eigenspace_iff.1 h.1, smul_smul, aeval_X, eval_mul, eval_C, eval_pow, eval_X, LinearMap.map_smulₛₗ,
  RingHom.id_apply, mul_comm]
[GOAL]
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
μ : K
h : HasEigenvalue f μ
⊢ IsRoot (minpoly K f) μ
[PROOFSTEP]
rcases(Submodule.ne_bot_iff _).1 h with ⟨w, ⟨H, ne0⟩⟩
[GOAL]
case intro.intro
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
μ : K
h : HasEigenvalue f μ
w : V
H : w ∈ eigenspace f μ
ne0 : w ≠ 0
⊢ IsRoot (minpoly K f) μ
[PROOFSTEP]
refine' Or.resolve_right (smul_eq_zero.1 _) ne0
[GOAL]
case intro.intro
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
μ : K
h : HasEigenvalue f μ
w : V
H : w ∈ eigenspace f μ
ne0 : w ≠ 0
⊢ eval μ (minpoly K f) • w = 0
[PROOFSTEP]
simp [← aeval_apply_of_hasEigenvector ⟨H, ne0⟩, minpoly.aeval K f]
[GOAL]
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : IsRoot (minpoly K f) μ
⊢ HasEigenvalue f μ
[PROOFSTEP]
cases' dvd_iff_isRoot.2 h with p hp
[GOAL]
case intro
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : IsRoot (minpoly K f) μ
p : K[X]
hp : minpoly K f = (X - ↑C μ) * p
⊢ HasEigenvalue f μ
[PROOFSTEP]
rw [HasEigenvalue, eigenspace]
[GOAL]
case intro
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : IsRoot (minpoly K f) μ
p : K[X]
hp : minpoly K f = (X - ↑C μ) * p
⊢ LinearMap.ker (f - ↑(algebraMap K (End K V)) μ) ≠ ⊥
[PROOFSTEP]
intro con
[GOAL]
case intro
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : IsRoot (minpoly K f) μ
p : K[X]
hp : minpoly K f = (X - ↑C μ) * p
con : LinearMap.ker (f - ↑(algebraMap K (End K V)) μ) = ⊥
⊢ False
[PROOFSTEP]
cases' (LinearMap.isUnit_iff_ker_eq_bot _).2 con with u hu
[GOAL]
case intro.intro
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : IsRoot (minpoly K f) μ
p : K[X]
hp : minpoly K f = (X - ↑C μ) * p
con : LinearMap.ker (f - ↑(algebraMap K (End K V)) μ) = ⊥
u : (V →ₗ[K] V)ˣ
hu : ↑u = f - ↑(algebraMap K (End K V)) μ
⊢ False
[PROOFSTEP]
have p_ne_0 : p ≠ 0 := by
  intro con
  apply minpoly.ne_zero f.isIntegral
  rw [hp, con, mul_zero]
[GOAL]
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : IsRoot (minpoly K f) μ
p : K[X]
hp : minpoly K f = (X - ↑C μ) * p
con : LinearMap.ker (f - ↑(algebraMap K (End K V)) μ) = ⊥
u : (V →ₗ[K] V)ˣ
hu : ↑u = f - ↑(algebraMap K (End K V)) μ
⊢ p ≠ 0
[PROOFSTEP]
intro con
[GOAL]
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : IsRoot (minpoly K f) μ
p : K[X]
hp : minpoly K f = (X - ↑C μ) * p
con✝ : LinearMap.ker (f - ↑(algebraMap K (End K V)) μ) = ⊥
u : (V →ₗ[K] V)ˣ
hu : ↑u = f - ↑(algebraMap K (End K V)) μ
con : p = 0
⊢ False
[PROOFSTEP]
apply minpoly.ne_zero f.isIntegral
[GOAL]
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : IsRoot (minpoly K f) μ
p : K[X]
hp : minpoly K f = (X - ↑C μ) * p
con✝ : LinearMap.ker (f - ↑(algebraMap K (End K V)) μ) = ⊥
u : (V →ₗ[K] V)ˣ
hu : ↑u = f - ↑(algebraMap K (End K V)) μ
con : p = 0
⊢ minpoly K f = 0
[PROOFSTEP]
rw [hp, con, mul_zero]
[GOAL]
case intro.intro
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : IsRoot (minpoly K f) μ
p : K[X]
hp : minpoly K f = (X - ↑C μ) * p
con : LinearMap.ker (f - ↑(algebraMap K (End K V)) μ) = ⊥
u : (V →ₗ[K] V)ˣ
hu : ↑u = f - ↑(algebraMap K (End K V)) μ
p_ne_0 : p ≠ 0
⊢ False
[PROOFSTEP]
have : (aeval f) p = 0 := by
  have h_aeval := minpoly.aeval K f
  revert h_aeval
  simp [hp, ← hu]
[GOAL]
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : IsRoot (minpoly K f) μ
p : K[X]
hp : minpoly K f = (X - ↑C μ) * p
con : LinearMap.ker (f - ↑(algebraMap K (End K V)) μ) = ⊥
u : (V →ₗ[K] V)ˣ
hu : ↑u = f - ↑(algebraMap K (End K V)) μ
p_ne_0 : p ≠ 0
⊢ ↑(aeval f) p = 0
[PROOFSTEP]
have h_aeval := minpoly.aeval K f
[GOAL]
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : IsRoot (minpoly K f) μ
p : K[X]
hp : minpoly K f = (X - ↑C μ) * p
con : LinearMap.ker (f - ↑(algebraMap K (End K V)) μ) = ⊥
u : (V →ₗ[K] V)ˣ
hu : ↑u = f - ↑(algebraMap K (End K V)) μ
p_ne_0 : p ≠ 0
h_aeval : ↑(aeval f) (minpoly K f) = 0
⊢ ↑(aeval f) p = 0
[PROOFSTEP]
revert h_aeval
[GOAL]
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : IsRoot (minpoly K f) μ
p : K[X]
hp : minpoly K f = (X - ↑C μ) * p
con : LinearMap.ker (f - ↑(algebraMap K (End K V)) μ) = ⊥
u : (V →ₗ[K] V)ˣ
hu : ↑u = f - ↑(algebraMap K (End K V)) μ
p_ne_0 : p ≠ 0
⊢ ↑(aeval f) (minpoly K f) = 0 → ↑(aeval f) p = 0
[PROOFSTEP]
simp [hp, ← hu]
[GOAL]
case intro.intro
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : IsRoot (minpoly K f) μ
p : K[X]
hp : minpoly K f = (X - ↑C μ) * p
con : LinearMap.ker (f - ↑(algebraMap K (End K V)) μ) = ⊥
u : (V →ₗ[K] V)ˣ
hu : ↑u = f - ↑(algebraMap K (End K V)) μ
p_ne_0 : p ≠ 0
this : ↑(aeval f) p = 0
⊢ False
[PROOFSTEP]
have h_deg := minpoly.degree_le_of_ne_zero K f p_ne_0 this
[GOAL]
case intro.intro
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : IsRoot (minpoly K f) μ
p : K[X]
hp : minpoly K f = (X - ↑C μ) * p
con : LinearMap.ker (f - ↑(algebraMap K (End K V)) μ) = ⊥
u : (V →ₗ[K] V)ˣ
hu : ↑u = f - ↑(algebraMap K (End K V)) μ
p_ne_0 : p ≠ 0
this : ↑(aeval f) p = 0
h_deg : degree (minpoly K f) ≤ degree p
⊢ False
[PROOFSTEP]
rw [hp, degree_mul, degree_X_sub_C, Polynomial.degree_eq_natDegree p_ne_0] at h_deg 
[GOAL]
case intro.intro
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : IsRoot (minpoly K f) μ
p : K[X]
hp : minpoly K f = (X - ↑C μ) * p
con : LinearMap.ker (f - ↑(algebraMap K (End K V)) μ) = ⊥
u : (V →ₗ[K] V)ˣ
hu : ↑u = f - ↑(algebraMap K (End K V)) μ
p_ne_0 : p ≠ 0
this : ↑(aeval f) p = 0
h_deg : 1 + ↑(natDegree p) ≤ ↑(natDegree p)
⊢ False
[PROOFSTEP]
norm_cast at h_deg 
[GOAL]
case intro.intro
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : IsRoot (minpoly K f) μ
p : K[X]
hp : minpoly K f = (X - ↑C μ) * p
con : LinearMap.ker (f - ↑(algebraMap K (End K V)) μ) = ⊥
u : (V →ₗ[K] V)ˣ
hu : ↑u = f - ↑(algebraMap K (End K V)) μ
p_ne_0 : p ≠ 0
this : ↑(aeval f) p = 0
h_deg : 1 + natDegree p ≤ natDegree p
⊢ False
[PROOFSTEP]
linarith
[GOAL]
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f✝ : End K V
μ : K
f : End K V
⊢ Set.Finite {μ | eigenspace f μ ≠ ⊥}
[PROOFSTEP]
have h : minpoly K f ≠ 0 := minpoly.ne_zero f.isIntegral
[GOAL]
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f✝ : End K V
μ : K
f : End K V
h : minpoly K f ≠ 0
⊢ Set.Finite {μ | eigenspace f μ ≠ ⊥}
[PROOFSTEP]
convert (minpoly K f).rootSet_finite K
[GOAL]
case h.e'_2
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f✝ : End K V
μ : K
f : End K V
h : minpoly K f ≠ 0
⊢ {μ | eigenspace f μ ≠ ⊥} = rootSet (minpoly K f) K
[PROOFSTEP]
ext μ
[GOAL]
case h.e'_2.h
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f✝ : End K V
μ✝ : K
f : End K V
h : minpoly K f ≠ 0
μ : K
⊢ μ ∈ {μ | eigenspace f μ ≠ ⊥} ↔ μ ∈ rootSet (minpoly K f) K
[PROOFSTEP]
rw [Set.mem_setOf_eq, ← HasEigenvalue, hasEigenvalue_iff_isRoot, mem_rootSet_of_ne h, IsRoot, coe_aeval_eq_eval]
