[GOAL]
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
⊢ ↑(aeval f) (charpoly f) = 0
[PROOFSTEP]
apply (LinearEquiv.map_eq_zero_iff (algEquivMatrix (chooseBasis R M)).toLinearEquiv).1
[GOAL]
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
⊢ ↑(AlgEquiv.toLinearEquiv (algEquivMatrix (chooseBasis R M))) (↑(aeval f) (charpoly f)) = 0
[PROOFSTEP]
rw [AlgEquiv.toLinearEquiv_apply, ← AlgEquiv.coe_algHom, ← Polynomial.aeval_algHom_apply _ _ _, charpoly_def]
[GOAL]
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
⊢ ↑(aeval (↑↑(algEquivMatrix (chooseBasis R M)) f))
      (Matrix.charpoly (↑(toMatrix (chooseBasis R M) (chooseBasis R M)) f)) =
    0
[PROOFSTEP]
exact Matrix.aeval_self_charpoly _
[GOAL]
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
k : ℕ
⊢ f ^ k = ↑(aeval f) (X ^ k %ₘ charpoly f)
[PROOFSTEP]
rw [← aeval_eq_aeval_mod_charpoly, map_pow, aeval_X]
[GOAL]
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
hf : Function.Injective ↑f
⊢ coeff (minpoly R f) 0 ≠ 0
[PROOFSTEP]
intro h
[GOAL]
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
hf : Function.Injective ↑f
h : coeff (minpoly R f) 0 = 0
⊢ False
[PROOFSTEP]
obtain ⟨P, hP⟩ := X_dvd_iff.2 h
[GOAL]
case intro
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
hf : Function.Injective ↑f
h : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
⊢ False
[PROOFSTEP]
have hdegP : P.degree < (minpoly R f).degree := by
  rw [hP, mul_comm]
  refine' degree_lt_degree_mul_X fun h => _
  rw [h, mul_zero] at hP 
  exact minpoly.ne_zero (isIntegral f) hP
[GOAL]
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
hf : Function.Injective ↑f
h : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
⊢ degree P < degree (minpoly R f)
[PROOFSTEP]
rw [hP, mul_comm]
[GOAL]
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
hf : Function.Injective ↑f
h : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
⊢ degree P < degree (P * X)
[PROOFSTEP]
refine' degree_lt_degree_mul_X fun h => _
[GOAL]
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
hf : Function.Injective ↑f
h✝ : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
h : P = 0
⊢ False
[PROOFSTEP]
rw [h, mul_zero] at hP 
[GOAL]
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
hf : Function.Injective ↑f
h✝ : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = 0
h : P = 0
⊢ False
[PROOFSTEP]
exact minpoly.ne_zero (isIntegral f) hP
[GOAL]
case intro
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
hf : Function.Injective ↑f
h : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
hdegP : degree P < degree (minpoly R f)
⊢ False
[PROOFSTEP]
have hPmonic : P.Monic :=
  by
  suffices (minpoly R f).Monic by rwa [Monic.def, hP, mul_comm, leadingCoeff_mul_X, ← Monic.def] at this 
  exact minpoly.monic (isIntegral f)
[GOAL]
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
hf : Function.Injective ↑f
h : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
hdegP : degree P < degree (minpoly R f)
⊢ Monic P
[PROOFSTEP]
suffices (minpoly R f).Monic by rwa [Monic.def, hP, mul_comm, leadingCoeff_mul_X, ← Monic.def] at this 
[GOAL]
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
hf : Function.Injective ↑f
h : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
hdegP : degree P < degree (minpoly R f)
this : Monic (minpoly R f)
⊢ Monic P
[PROOFSTEP]
rwa [Monic.def, hP, mul_comm, leadingCoeff_mul_X, ← Monic.def] at this 
[GOAL]
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
hf : Function.Injective ↑f
h : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
hdegP : degree P < degree (minpoly R f)
⊢ Monic (minpoly R f)
[PROOFSTEP]
exact minpoly.monic (isIntegral f)
[GOAL]
case intro
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
hf : Function.Injective ↑f
h : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
hdegP : degree P < degree (minpoly R f)
hPmonic : Monic P
⊢ False
[PROOFSTEP]
have hzero : aeval f (minpoly R f) = 0 := minpoly.aeval _ _
[GOAL]
case intro
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
hf : Function.Injective ↑f
h : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
hdegP : degree P < degree (minpoly R f)
hPmonic : Monic P
hzero : ↑(aeval f) (minpoly R f) = 0
⊢ False
[PROOFSTEP]
simp only [hP, mul_eq_comp, ext_iff, hf, aeval_X, map_eq_zero_iff, coe_comp, AlgHom.map_mul, zero_apply,
  Function.comp_apply] at hzero 
[GOAL]
case intro
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
hf : Function.Injective ↑f
h : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
hdegP : degree P < degree (minpoly R f)
hPmonic : Monic P
hzero : ∀ (x : M), ↑(↑(aeval f) P) x = 0
⊢ False
[PROOFSTEP]
exact not_le.2 hdegP (minpoly.min _ _ hPmonic (ext hzero))
