[GOAL]
R : Type u
inst✝⁶ : CommRing R
n : Type v
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
⊢ charpoly (↑(leftMulMatrix h.basis) h.gen) = minpoly R h.gen
[PROOFSTEP]
cases subsingleton_or_nontrivial R
[GOAL]
case inl
R : Type u
inst✝⁶ : CommRing R
n : Type v
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
h✝ : Subsingleton R
⊢ charpoly (↑(leftMulMatrix h.basis) h.gen) = minpoly R h.gen
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
case inr
R : Type u
inst✝⁶ : CommRing R
n : Type v
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
h✝ : Nontrivial R
⊢ charpoly (↑(leftMulMatrix h.basis) h.gen) = minpoly R h.gen
[PROOFSTEP]
apply minpoly.unique' R h.gen (charpoly_monic _)
[GOAL]
case inr.hp
R : Type u
inst✝⁶ : CommRing R
n : Type v
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
h✝ : Nontrivial R
⊢ ↑(aeval h.gen) (charpoly (↑(leftMulMatrix h.basis) h.gen)) = 0
[PROOFSTEP]
apply (injective_iff_map_eq_zero (G := S) (leftMulMatrix _)).mp (leftMulMatrix_injective h.basis)
[GOAL]
case inr.hp.a
R : Type u
inst✝⁶ : CommRing R
n : Type v
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
h✝ : Nontrivial R
⊢ ↑(leftMulMatrix h.basis) (↑(aeval h.gen) (charpoly (↑(leftMulMatrix h.basis) h.gen))) = 0
[PROOFSTEP]
rw [← Polynomial.aeval_algHom_apply, aeval_self_charpoly]
[GOAL]
case inr.hl
R : Type u
inst✝⁶ : CommRing R
n : Type v
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
h✝ : Nontrivial R
⊢ ∀ (q : R[X]), degree q < degree (charpoly (↑(leftMulMatrix h.basis) h.gen)) → q = 0 ∨ ↑(aeval h.gen) q ≠ 0
[PROOFSTEP]
refine' fun q hq => or_iff_not_imp_left.2 fun h0 => _
[GOAL]
case inr.hl
R : Type u
inst✝⁶ : CommRing R
n : Type v
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
h✝ : Nontrivial R
q : R[X]
hq : degree q < degree (charpoly (↑(leftMulMatrix h.basis) h.gen))
h0 : ¬q = 0
⊢ ↑(aeval h.gen) q ≠ 0
[PROOFSTEP]
rw [Matrix.charpoly_degree_eq_dim, Fintype.card_fin] at hq 
[GOAL]
case inr.hl
R : Type u
inst✝⁶ : CommRing R
n : Type v
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
h✝ : Nontrivial R
q : R[X]
hq : degree q < ↑h.dim
h0 : ¬q = 0
⊢ ↑(aeval h.gen) q ≠ 0
[PROOFSTEP]
contrapose! hq
[GOAL]
case inr.hl
R : Type u
inst✝⁶ : CommRing R
n : Type v
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
h✝ : Nontrivial R
q : R[X]
h0 : ¬q = 0
hq : ↑(aeval h.gen) q = 0
⊢ ↑h.dim ≤ degree q
[PROOFSTEP]
exact h.dim_le_degree_of_root h0 hq
