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

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
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
cases subsingleton_or_nontrivial R
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

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
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
apply minpoly.unique' R h.gen (charpoly_monic _)
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
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
refine' fun q hq => or_iff_not_imp_left.2 fun h0 => _
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
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
rw [Matrix.charpoly_degree_eq_dim, Fintype.card_fin] at hq
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
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
contrapose! hq
no goals
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
exact h.dim_le_degree_of_root h0 hq
no goals
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
apply Subsingleton.elim
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
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
apply (injective_iff_map_eq_zero (G := S) (leftMulMatrix _)).mp
  (leftMulMatrix_injective h.basis)
no goals
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
rw [← Polynomial.aeval_algHom_apply, aeval_self_charpoly]