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
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
intro h
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
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
obtain ⟨P, hP⟩ := X_dvd_iff.2 h
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
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
have hdegP : P.degree < (minpoly R f).degree := by
  rw [hP, mul_comm]
  refine' degree_lt_degree_mul_X fun h => _
  rw [h, MulZeroClass.mul_zero] at hP
  exact minpoly.ne_zero (isIntegral f) hP
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
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
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)
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
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
have hzero : aeval f (minpoly R f) = 0 := minpoly.aeval _ _
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
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
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
no goals
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
exact not_le.2 hdegP (minpoly.min _ _ hPmonic (ext hzero))
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)
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)
rw [hP, mul_comm]
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
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)
refine' degree_lt_degree_mul_X fun h => _
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
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
rw [h, MulZeroClass.mul_zero] at hP
no goals
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
exact minpoly.ne_zero (isIntegral f) hP
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)
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
suffices (minpoly R f).Monic by
  rwa [Monic.def, hP, mul_comm, leadingCoeff_mul_X, ← Monic.def] at this
no goals
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)
exact minpoly.monic (isIntegral f)
no goals
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
rwa [Monic.def, hP, mul_comm, leadingCoeff_mul_X, ← Monic.def] at this