case inl
R : Type ?u.145334
S : Type u_2
T : Type ?u.145340
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.145646
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.146068
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Subsingleton A
⊢ ↑(Algebra.leftMulMatrix pb.basis) pb.gen =
    ↑Matrix.of fun i j => if ↑j + 1 = pb.dim then -coeff (minpolyGen pb) ↑i else if ↑i = ↑j + 1 then 1 else 0

case inr
R : Type ?u.145334
S : Type u_2
T : Type ?u.145340
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.145646
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.146068
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
⊢ ↑(Algebra.leftMulMatrix pb.basis) pb.gen =
    ↑Matrix.of fun i j => if ↑j + 1 = pb.dim then -coeff (minpolyGen pb) ↑i else if ↑i = ↑j + 1 then 1 else 0
R : Type ?u.145334
S : Type u_2
T : Type ?u.145340
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.145646
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.146068
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
⊢ ↑(Algebra.leftMulMatrix pb.basis) pb.gen =
    ↑Matrix.of fun i j => if ↑j + 1 = pb.dim then -coeff (minpolyGen pb) ↑i else if ↑i = ↑j + 1 then 1 else 0
cases subsingleton_or_nontrivial A
case inr
R : Type ?u.145334
S : Type u_2
T : Type ?u.145340
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.145646
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.146068
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
⊢ ↑(Algebra.lmul A S) pb.gen =
    ↑(Matrix.toLin pb.basis pb.basis)
      (↑Matrix.of fun i j => if ↑j + 1 = pb.dim then -coeff (minpolyGen pb) ↑i else if ↑i = ↑j + 1 then 1 else 0)
case inr
R : Type ?u.145334
S : Type u_2
T : Type ?u.145340
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.145646
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.146068
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
⊢ ↑(Algebra.leftMulMatrix pb.basis) pb.gen =
    ↑Matrix.of fun i j => if ↑j + 1 = pb.dim then -coeff (minpolyGen pb) ↑i else if ↑i = ↑j + 1 then 1 else 0
rw [Algebra.leftMulMatrix_apply, ← LinearEquiv.eq_symm_apply, LinearMap.toMatrix_symm]
case inr
R : Type ?u.145334
S : Type u_2
T : Type ?u.145340
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.145646
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.146068
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
⊢ ↑(↑(Algebra.lmul A S) pb.gen) (↑pb.basis k) =
    ↑(↑(Matrix.toLin pb.basis pb.basis)
          (↑Matrix.of fun i j => if ↑j + 1 = pb.dim then -coeff (minpolyGen pb) ↑i else if ↑i = ↑j + 1 then 1 else 0))
      (↑pb.basis k)
case inr
R : Type ?u.145334
S : Type u_2
T : Type ?u.145340
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.145646
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.146068
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
⊢ ↑(Algebra.lmul A S) pb.gen =
    ↑(Matrix.toLin pb.basis pb.basis)
      (↑Matrix.of fun i j => if ↑j + 1 = pb.dim then -coeff (minpolyGen pb) ↑i else if ↑i = ↑j + 1 then 1 else 0)
refine' pb.basis.ext fun k => _
case inr
R : Type ?u.145334
S : Type u_2
T : Type ?u.145340
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.145646
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.146068
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
⊢ ↑(↑(Algebra.lmul A S) pb.gen) (pb.gen ^ ↑k) =
    ∑ x : Fin pb.dim,
      (if ↑k + 1 = pb.dim then -coeff (minpolyGen pb) ↑x else if ↑x = ↑k + 1 then 1 else 0) • pb.gen ^ ↑x
case inr
R : Type ?u.145334
S : Type u_2
T : Type ?u.145340
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.145646
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.146068
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
⊢ ↑(↑(Algebra.lmul A S) pb.gen) (↑pb.basis k) =
    ↑(↑(Matrix.toLin pb.basis pb.basis)
          (↑Matrix.of fun i j => if ↑j + 1 = pb.dim then -coeff (minpolyGen pb) ↑i else if ↑i = ↑j + 1 then 1 else 0))
      (↑pb.basis k)
simp_rw [Matrix.toLin_self, Matrix.of_apply, pb.basis_eq_pow]
case inr
R : Type ?u.145334
S : Type u_2
T : Type ?u.145340
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.145646
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.146068
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
⊢ pb.gen ^ (↑k + 1) =
    ∑ x : Fin pb.dim,
      (if ↑k + 1 = pb.dim then -coeff (minpolyGen pb) ↑x else if ↑x = ↑k + 1 then 1 else 0) • pb.gen ^ ↑x
case inr
R : Type ?u.145334
S : Type u_2
T : Type ?u.145340
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.145646
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.146068
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
⊢ ↑(↑(Algebra.lmul A S) pb.gen) (pb.gen ^ ↑k) =
    ∑ x : Fin pb.dim,
      (if ↑k + 1 = pb.dim then -coeff (minpolyGen pb) ↑x else if ↑x = ↑k + 1 then 1 else 0) • pb.gen ^ ↑x
apply (pow_succ _ _).symm.trans
case inr.inl
R : Type ?u.145334
S : Type u_2
T : Type ?u.145340
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.145646
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.146068
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ↑k + 1 = pb.dim
⊢ pb.gen ^ (↑k + 1) = ∑ x : Fin pb.dim, -coeff (minpolyGen pb) ↑x • pb.gen ^ ↑x

case inr.inr
R : Type ?u.145334
S : Type u_2
T : Type ?u.145340
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.145646
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.146068
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ¬↑k + 1 = pb.dim
⊢ pb.gen ^ (↑k + 1) = ∑ x : Fin pb.dim, (if ↑x = ↑k + 1 then 1 else 0) • pb.gen ^ ↑x
case inr
R : Type ?u.145334
S : Type u_2
T : Type ?u.145340
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.145646
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.146068
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
⊢ pb.gen ^ (↑k + 1) =
    ∑ x : Fin pb.dim,
      (if ↑k + 1 = pb.dim then -coeff (minpolyGen pb) ↑x else if ↑x = ↑k + 1 then 1 else 0) • pb.gen ^ ↑x
split_ifs with h
no goals
case inl
R : Type ?u.145334
S : Type u_2
T : Type ?u.145340
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.145646
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.146068
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Subsingleton A
⊢ ↑(Algebra.leftMulMatrix pb.basis) pb.gen =
    ↑Matrix.of fun i j => if ↑j + 1 = pb.dim then -coeff (minpolyGen pb) ↑i else if ↑i = ↑j + 1 then 1 else 0
apply Subsingleton.elim
case inr.inl
R : Type ?u.145334
S : Type u_2
T : Type ?u.145340
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.145646
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.146068
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ↑k + 1 = pb.dim
⊢ pb.gen ^ pb.dim + ∑ x : Fin pb.dim, coeff (minpolyGen pb) ↑x • pb.gen ^ ↑x = 0
case inr.inl
R : Type ?u.145334
S : Type u_2
T : Type ?u.145340
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.145646
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.146068
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ↑k + 1 = pb.dim
⊢ pb.gen ^ (↑k + 1) = ∑ x : Fin pb.dim, -coeff (minpolyGen pb) ↑x • pb.gen ^ ↑x
simp_rw [h, neg_smul, Finset.sum_neg_distrib, eq_neg_iff_add_eq_zero]
case h.e'_2
R : Type ?u.145334
S : Type u_2
T : Type ?u.145340
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.145646
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.146068
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ↑k + 1 = pb.dim
⊢ pb.gen ^ pb.dim + ∑ x : Fin pb.dim, coeff (minpolyGen pb) ↑x • pb.gen ^ ↑x = ↑(aeval pb.gen) (minpolyGen pb)
case inr.inl
R : Type ?u.145334
S : Type u_2
T : Type ?u.145340
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.145646
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.146068
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ↑k + 1 = pb.dim
⊢ pb.gen ^ pb.dim + ∑ x : Fin pb.dim, coeff (minpolyGen pb) ↑x • pb.gen ^ ↑x = 0
convert pb.aeval_minpolyGen
no goals
case h.e'_2
R : Type ?u.145334
S : Type u_2
T : Type ?u.145340
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.145646
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.146068
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ↑k + 1 = pb.dim
⊢ pb.gen ^ pb.dim + ∑ x : Fin pb.dim, coeff (minpolyGen pb) ↑x • pb.gen ^ ↑x = ↑(aeval pb.gen) (minpolyGen pb)
rw [add_comm, aeval_eq_sum_range, Finset.sum_range_succ, ← leadingCoeff,
  pb.minpolyGen_monic.leadingCoeff, one_smul, natDegree_minpolyGen, Finset.sum_range]
case inr.inr.hc
R : Type ?u.145334
S : Type u_2
T : Type ?u.145340
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.145646
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.146068
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ¬↑k + 1 = pb.dim
⊢ ↑{ val := ↑k + 1, isLt := (_ : ↑k + 1 < pb.dim) } = ↑k + 1

case inr.inr
R : Type ?u.145334
S : Type u_2
T : Type ?u.145340
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.145646
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.146068
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ¬↑k + 1 = pb.dim
⊢ ∀ (x : Fin pb.dim),
    x ≠ { val := ↑k + 1, isLt := (_ : ↑k + 1 < pb.dim) } → (if ↑x = ↑k + 1 then 1 else 0) • pb.gen ^ ↑x = 0
case inr.inr
R : Type ?u.145334
S : Type u_2
T : Type ?u.145340
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.145646
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.146068
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ¬↑k + 1 = pb.dim
⊢ pb.gen ^ (↑k + 1) = ∑ x : Fin pb.dim, (if ↑x = ↑k + 1 then 1 else 0) • pb.gen ^ ↑x
rw [Fintype.sum_eq_single (⟨(k : ℕ) + 1, lt_of_le_of_ne k.2 h⟩ : Fin pb.dim), if_pos, one_smul]
case inr.inr
R : Type ?u.145334
S : Type u_2
T : Type ?u.145340
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.145646
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.146068
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ¬↑k + 1 = pb.dim
x : Fin pb.dim
hx : x ≠ { val := ↑k + 1, isLt := (_ : ↑k + 1 < pb.dim) }
⊢ (if ↑x = ↑k + 1 then 1 else 0) • pb.gen ^ ↑x = 0
case inr.inr
R : Type ?u.145334
S : Type u_2
T : Type ?u.145340
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.145646
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.146068
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ¬↑k + 1 = pb.dim
⊢ ∀ (x : Fin pb.dim),
    x ≠ { val := ↑k + 1, isLt := (_ : ↑k + 1 < pb.dim) } → (if ↑x = ↑k + 1 then 1 else 0) • pb.gen ^ ↑x = 0
intro x hx
case inr.inr.hnc
R : Type ?u.145334
S : Type u_2
T : Type ?u.145340
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.145646
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.146068
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ¬↑k + 1 = pb.dim
x : Fin pb.dim
hx : x ≠ { val := ↑k + 1, isLt := (_ : ↑k + 1 < pb.dim) }
⊢ ¬↑x = ↑k + 1
case inr.inr
R : Type ?u.145334
S : Type u_2
T : Type ?u.145340
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.145646
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.146068
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ¬↑k + 1 = pb.dim
x : Fin pb.dim
hx : x ≠ { val := ↑k + 1, isLt := (_ : ↑k + 1 < pb.dim) }
⊢ (if ↑x = ↑k + 1 then 1 else 0) • pb.gen ^ ↑x = 0
rw [if_neg, zero_smul]
no goals
case inr.inr.hnc
R : Type ?u.145334
S : Type u_2
T : Type ?u.145340
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.145646
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.146068
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ¬↑k + 1 = pb.dim
x : Fin pb.dim
hx : x ≠ { val := ↑k + 1, isLt := (_ : ↑k + 1 < pb.dim) }
⊢ ¬↑x = ↑k + 1
apply mt Fin.ext hx
no goals
case inr.inr.hc
R : Type ?u.145334
S : Type u_2
T : Type ?u.145340
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.145646
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.146068
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ¬↑k + 1 = pb.dim
⊢ ↑{ val := ↑k + 1, isLt := (_ : ↑k + 1 < pb.dim) } = ↑k + 1
rfl