[STATEMENT]
lemma char_poly_similar: assumes "similar_mat A (B :: 'a :: comm_ring_1 mat)"
  shows "char_poly A = char_poly B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. char_poly A = char_poly B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. char_poly A = char_poly B
[PROOF STEP]
from similar_matD[OF assms]
[PROOF STATE]
proof (chain)
picking this:
\<exists>n P Q. {A, B, P, Q} \<subseteq> carrier_mat n n \<and> P * Q = 1\<^sub>m n \<and> Q * P = 1\<^sub>m n \<and> A = P * B * Q
[PROOF STEP]
obtain n P Q where
  carr: "{A, B, P, Q} \<subseteq> carrier_mat n n" (is "_ \<subseteq> ?C")
  and PQ: "P * Q = 1\<^sub>m n"
  and AB: "A = P * B * Q"
[PROOF STATE]
proof (prove)
using this:
\<exists>n P Q. {A, B, P, Q} \<subseteq> carrier_mat n n \<and> P * Q = 1\<^sub>m n \<and> Q * P = 1\<^sub>m n \<and> A = P * B * Q

goal (1 subgoal):
 1. (\<And>P Q n. \<lbrakk>{A, B, P, Q} \<subseteq> carrier_mat n n; P * Q = 1\<^sub>m n; A = P * B * Q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{A, B, P, Q} \<subseteq> carrier_mat n n
P * Q = 1\<^sub>m n
A = P * B * Q

goal (1 subgoal):
 1. char_poly A = char_poly B
[PROOF STEP]
hence A: "A \<in> ?C" and B: "B \<in> ?C" and P: "P \<in> ?C" and Q: "Q \<in> ?C"
[PROOF STATE]
proof (prove)
using this:
{A, B, P, Q} \<subseteq> carrier_mat n n
P * Q = 1\<^sub>m n
A = P * B * Q

goal (1 subgoal):
 1. (A \<in> carrier_mat n n &&& B \<in> carrier_mat n n) &&& P \<in> carrier_mat n n &&& Q \<in> carrier_mat n n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<in> carrier_mat n n
B \<in> carrier_mat n n
P \<in> carrier_mat n n
Q \<in> carrier_mat n n

goal (1 subgoal):
 1. char_poly A = char_poly B
[PROOF STEP]
let ?m = "\<lambda> a. [: -a :]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. char_poly A = char_poly B
[PROOF STEP]
let ?P = "map_mat (\<lambda> a. [: a :]) P"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. char_poly A = char_poly B
[PROOF STEP]
let ?Q = "map_mat (\<lambda> a. [: a :]) Q"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. char_poly A = char_poly B
[PROOF STEP]
let ?B = "map_mat ?m B"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. char_poly A = char_poly B
[PROOF STEP]
let ?I = "map_mat (\<lambda> a. [: a :]) (1\<^sub>m n)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. char_poly A = char_poly B
[PROOF STEP]
let ?XI = "[:0, 1:] \<cdot>\<^sub>m 1\<^sub>m n"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. char_poly A = char_poly B
[PROOF STEP]
from A B
[PROOF STATE]
proof (chain)
picking this:
A \<in> carrier_mat n n
B \<in> carrier_mat n n
[PROOF STEP]
have dim: "dim_row A = n" "dim_row B = n"
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n
B \<in> carrier_mat n n

goal (1 subgoal):
 1. dim_row A = n &&& dim_row B = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dim_row A = n
dim_row B = n

goal (1 subgoal):
 1. char_poly A = char_poly B
[PROOF STEP]
have cong: "\<And> x y z. x = y \<Longrightarrow> x * z = y * z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y z. x = y \<Longrightarrow> x * z = y * z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x3 = ?y3 \<Longrightarrow> ?x3 * ?z3 = ?y3 * ?z3

goal (1 subgoal):
 1. char_poly A = char_poly B
[PROOF STEP]
have id: "?m = (\<lambda> a :: 'a. [: a :] * [: -1 :])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>a. [:- a:]) = (\<lambda>a. [:a:] * [:- (1::'a):])
[PROOF STEP]
by (intro ext, auto)
[PROOF STATE]
proof (state)
this:
(\<lambda>a. [:- a:]) = (\<lambda>a. [:a:] * [:- (1::'a):])

goal (1 subgoal):
 1. char_poly A = char_poly B
[PROOF STEP]
have "char_poly A = det (?XI + map_mat (\<lambda>a. [:- a:]) (P * B * Q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. char_poly A = det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) (P * B * Q))
[PROOF STEP]
unfolding
    char_poly_defs dim
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) = det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) (P * B * Q))
[PROOF STEP]
by (simp add: AB)
[PROOF STATE]
proof (state)
this:
char_poly A = det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) (P * B * Q))

goal (1 subgoal):
 1. char_poly A = char_poly B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
char_poly A = det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) (P * B * Q))

goal (1 subgoal):
 1. char_poly A = char_poly B
[PROOF STEP]
have "?XI = ?P * ?XI * ?Q" (is "_ = ?left")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n = map_mat (\<lambda>a. [:a:]) P * ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n) * map_mat (\<lambda>a. [:a:]) Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n = map_mat (\<lambda>a. [:a:]) P * ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n) * map_mat (\<lambda>a. [:a:]) Q
[PROOF STEP]
have "?P * ?XI = [:0, 1:] \<cdot>\<^sub>m (?P * 1\<^sub>m n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_mat (\<lambda>a. [:a:]) P * ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n) = [:0::'a, 1::'a:] \<cdot>\<^sub>m (map_mat (\<lambda>a. [:a:]) P * 1\<^sub>m n)
[PROOF STEP]
by (rule mult_smult_distrib[of _ n n _ n], insert P, auto)
[PROOF STATE]
proof (state)
this:
map_mat (\<lambda>a. [:a:]) P * ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n) = [:0::'a, 1::'a:] \<cdot>\<^sub>m (map_mat (\<lambda>a. [:a:]) P * 1\<^sub>m n)

goal (1 subgoal):
 1. [:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n = map_mat (\<lambda>a. [:a:]) P * ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n) * map_mat (\<lambda>a. [:a:]) Q
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map_mat (\<lambda>a. [:a:]) P * ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n) = [:0::'a, 1::'a:] \<cdot>\<^sub>m (map_mat (\<lambda>a. [:a:]) P * 1\<^sub>m n)

goal (1 subgoal):
 1. [:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n = map_mat (\<lambda>a. [:a:]) P * ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n) * map_mat (\<lambda>a. [:a:]) Q
[PROOF STEP]
have "?P * 1\<^sub>m n = ?P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_mat (\<lambda>a. [:a:]) P * 1\<^sub>m n = map_mat (\<lambda>a. [:a:]) P
[PROOF STEP]
using P
[PROOF STATE]
proof (prove)
using this:
P \<in> carrier_mat n n

goal (1 subgoal):
 1. map_mat (\<lambda>a. [:a:]) P * 1\<^sub>m n = map_mat (\<lambda>a. [:a:]) P
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map_mat (\<lambda>a. [:a:]) P * 1\<^sub>m n = map_mat (\<lambda>a. [:a:]) P

goal (1 subgoal):
 1. [:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n = map_mat (\<lambda>a. [:a:]) P * ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n) * map_mat (\<lambda>a. [:a:]) Q
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map_mat (\<lambda>a. [:a:]) P * 1\<^sub>m n = map_mat (\<lambda>a. [:a:]) P

goal (1 subgoal):
 1. [:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n = map_mat (\<lambda>a. [:a:]) P * ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n) * map_mat (\<lambda>a. [:a:]) Q
[PROOF STEP]
have "([: 0, 1:] \<cdot>\<^sub>m ?P) * ?Q = [: 0, 1:] \<cdot>\<^sub>m (?P * ?Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [:0::'a, 1::'a:] \<cdot>\<^sub>m map_mat (\<lambda>a. [:a:]) P * map_mat (\<lambda>a. [:a:]) Q = [:0::'a, 1::'a:] \<cdot>\<^sub>m (map_mat (\<lambda>a. [:a:]) P * map_mat (\<lambda>a. [:a:]) Q)
[PROOF STEP]
by (rule mult_smult_assoc_mat, insert P Q, auto)
[PROOF STATE]
proof (state)
this:
[:0::'a, 1::'a:] \<cdot>\<^sub>m map_mat (\<lambda>a. [:a:]) P * map_mat (\<lambda>a. [:a:]) Q = [:0::'a, 1::'a:] \<cdot>\<^sub>m (map_mat (\<lambda>a. [:a:]) P * map_mat (\<lambda>a. [:a:]) Q)

goal (1 subgoal):
 1. [:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n = map_mat (\<lambda>a. [:a:]) P * ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n) * map_mat (\<lambda>a. [:a:]) Q
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
[:0::'a, 1::'a:] \<cdot>\<^sub>m map_mat (\<lambda>a. [:a:]) P * map_mat (\<lambda>a. [:a:]) Q = [:0::'a, 1::'a:] \<cdot>\<^sub>m (map_mat (\<lambda>a. [:a:]) P * map_mat (\<lambda>a. [:a:]) Q)

goal (1 subgoal):
 1. [:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n = map_mat (\<lambda>a. [:a:]) P * ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n) * map_mat (\<lambda>a. [:a:]) Q
[PROOF STEP]
have "?P * ?Q = ?I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_mat (\<lambda>a. [:a:]) P * map_mat (\<lambda>a. [:a:]) Q = map_mat (\<lambda>a. [:a:]) (1\<^sub>m n)
[PROOF STEP]
unfolding PQ[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_mat (\<lambda>a. [:a:]) P * map_mat (\<lambda>a. [:a:]) Q = map_mat (\<lambda>a. [:a:]) (P * Q)
[PROOF STEP]
by (rule map_poly_mult[symmetric, OF P Q])
[PROOF STATE]
proof (state)
this:
map_mat (\<lambda>a. [:a:]) P * map_mat (\<lambda>a. [:a:]) Q = map_mat (\<lambda>a. [:a:]) (1\<^sub>m n)

goal (1 subgoal):
 1. [:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n = map_mat (\<lambda>a. [:a:]) P * ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n) * map_mat (\<lambda>a. [:a:]) Q
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map_mat (\<lambda>a. [:a:]) P * map_mat (\<lambda>a. [:a:]) Q = map_mat (\<lambda>a. [:a:]) (1\<^sub>m n)

goal (1 subgoal):
 1. [:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n = map_mat (\<lambda>a. [:a:]) P * ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n) * map_mat (\<lambda>a. [:a:]) Q
[PROOF STEP]
have "[: 0, 1:] \<cdot>\<^sub>m ?I = ?XI"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [:0::'b, 1::'b:] \<cdot>\<^sub>m map_mat (\<lambda>a. [:a:]) (1\<^sub>m n) = [:0::'b, 1::'b:] \<cdot>\<^sub>m 1\<^sub>m n
[PROOF STEP]
by rule auto
[PROOF STATE]
proof (state)
this:
[:0::?'b5, 1::?'b5:] \<cdot>\<^sub>m map_mat (\<lambda>a. [:a:]) (1\<^sub>m n) = [:0::?'b5, 1::?'b5:] \<cdot>\<^sub>m 1\<^sub>m n

goal (1 subgoal):
 1. [:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n = map_mat (\<lambda>a. [:a:]) P * ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n) * map_mat (\<lambda>a. [:a:]) Q
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
map_mat (\<lambda>a. [:a:]) P * ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n) * map_mat (\<lambda>a. [:a:]) Q = [:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
map_mat (\<lambda>a. [:a:]) P * ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n) * map_mat (\<lambda>a. [:a:]) Q = [:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n

goal (1 subgoal):
 1. [:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n = map_mat (\<lambda>a. [:a:]) P * ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n) * map_mat (\<lambda>a. [:a:]) Q
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
[:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n = map_mat (\<lambda>a. [:a:]) P * ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n) * map_mat (\<lambda>a. [:a:]) Q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n = map_mat (\<lambda>a. [:a:]) P * ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n) * map_mat (\<lambda>a. [:a:]) Q

goal (1 subgoal):
 1. char_poly A = char_poly B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
[:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n = map_mat (\<lambda>a. [:a:]) P * ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n) * map_mat (\<lambda>a. [:a:]) Q

goal (1 subgoal):
 1. char_poly A = char_poly B
[PROOF STEP]
have "map_mat ?m (P * B * Q) = ?P * ?B * ?Q" (is "_ = ?right")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_mat (\<lambda>a. [:- a:]) (P * B * Q) = map_mat (\<lambda>a. [:a:]) P * map_mat (\<lambda>a. [:- a:]) B * map_mat (\<lambda>a. [:a:]) Q
[PROOF STEP]
unfolding id
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_mat (\<lambda>a. [:a:] * [:- (1::'a):]) (P * B * Q) = map_mat (\<lambda>a. [:a:]) P * map_mat (\<lambda>a. [:a:] * [:- (1::'a):]) B * map_mat (\<lambda>a. [:a:]) Q
[PROOF STEP]
by (subst map_poly_mult[OF mult_carrier_mat[OF P B] Q],
      subst map_poly_mult(3)[OF P B], simp)
[PROOF STATE]
proof (state)
this:
map_mat (\<lambda>a. [:- a:]) (P * B * Q) = map_mat (\<lambda>a. [:a:]) P * map_mat (\<lambda>a. [:- a:]) B * map_mat (\<lambda>a. [:a:]) Q

goal (1 subgoal):
 1. char_poly A = char_poly B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map_mat (\<lambda>a. [:- a:]) (P * B * Q) = map_mat (\<lambda>a. [:a:]) P * map_mat (\<lambda>a. [:- a:]) B * map_mat (\<lambda>a. [:a:]) Q

goal (1 subgoal):
 1. char_poly A = char_poly B
[PROOF STEP]
have "?left + ?right = (?P * ?XI + ?P * ?B) * ?Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_mat (\<lambda>a. [:a:]) P * ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n) * map_mat (\<lambda>a. [:a:]) Q + map_mat (\<lambda>a. [:a:]) P * map_mat (\<lambda>a. [:- a:]) B * map_mat (\<lambda>a. [:a:]) Q = (map_mat (\<lambda>a. [:a:]) P * ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n) + map_mat (\<lambda>a. [:a:]) P * map_mat (\<lambda>a. [:- a:]) B) * map_mat (\<lambda>a. [:a:]) Q
[PROOF STEP]
by (rule add_mult_distrib_mat[symmetric, of _ n n], insert B P Q, auto)
[PROOF STATE]
proof (state)
this:
map_mat (\<lambda>a. [:a:]) P * ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n) * map_mat (\<lambda>a. [:a:]) Q + map_mat (\<lambda>a. [:a:]) P * map_mat (\<lambda>a. [:- a:]) B * map_mat (\<lambda>a. [:a:]) Q = (map_mat (\<lambda>a. [:a:]) P * ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n) + map_mat (\<lambda>a. [:a:]) P * map_mat (\<lambda>a. [:- a:]) B) * map_mat (\<lambda>a. [:a:]) Q

goal (1 subgoal):
 1. char_poly A = char_poly B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map_mat (\<lambda>a. [:a:]) P * ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n) * map_mat (\<lambda>a. [:a:]) Q + map_mat (\<lambda>a. [:a:]) P * map_mat (\<lambda>a. [:- a:]) B * map_mat (\<lambda>a. [:a:]) Q = (map_mat (\<lambda>a. [:a:]) P * ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n) + map_mat (\<lambda>a. [:a:]) P * map_mat (\<lambda>a. [:- a:]) B) * map_mat (\<lambda>a. [:a:]) Q

goal (1 subgoal):
 1. char_poly A = char_poly B
[PROOF STEP]
have "?P * ?XI + ?P * ?B = ?P * (?XI + ?B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_mat (\<lambda>a. [:a:]) P * ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n) + map_mat (\<lambda>a. [:a:]) P * map_mat (\<lambda>a. [:- a:]) B = map_mat (\<lambda>a. [:a:]) P * ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) B)
[PROOF STEP]
by (rule mult_add_distrib_mat[symmetric, of _ n n], insert B P Q, auto)
[PROOF STATE]
proof (state)
this:
map_mat (\<lambda>a. [:a:]) P * ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n) + map_mat (\<lambda>a. [:a:]) P * map_mat (\<lambda>a. [:- a:]) B = map_mat (\<lambda>a. [:a:]) P * ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) B)

goal (1 subgoal):
 1. char_poly A = char_poly B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map_mat (\<lambda>a. [:a:]) P * ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n) + map_mat (\<lambda>a. [:a:]) P * map_mat (\<lambda>a. [:- a:]) B = map_mat (\<lambda>a. [:a:]) P * ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) B)

goal (1 subgoal):
 1. char_poly A = char_poly B
[PROOF STEP]
have "det (?P * (?XI + ?B) * ?Q) = det ?P * det (?XI + ?B) * det ?Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (map_mat (\<lambda>a. [:a:]) P * ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) B) * map_mat (\<lambda>a. [:a:]) Q) = det (map_mat (\<lambda>a. [:a:]) P) * det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) B) * det (map_mat (\<lambda>a. [:a:]) Q)
[PROOF STEP]
by (rule trans[OF det_mult[of _ n] cong[OF det_mult]], insert P Q B, auto)
[PROOF STATE]
proof (state)
this:
det (map_mat (\<lambda>a. [:a:]) P * ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) B) * map_mat (\<lambda>a. [:a:]) Q) = det (map_mat (\<lambda>a. [:a:]) P) * det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) B) * det (map_mat (\<lambda>a. [:a:]) Q)

goal (1 subgoal):
 1. char_poly A = char_poly B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
det (map_mat (\<lambda>a. [:a:]) P * ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) B) * map_mat (\<lambda>a. [:a:]) Q) = det (map_mat (\<lambda>a. [:a:]) P) * det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) B) * det (map_mat (\<lambda>a. [:a:]) Q)

goal (1 subgoal):
 1. char_poly A = char_poly B
[PROOF STEP]
have "\<dots> = (det ?P * det ?Q) * det (?XI + ?B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (map_mat (\<lambda>a. [:a:]) P) * det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) B) * det (map_mat (\<lambda>a. [:a:]) Q) = det (map_mat (\<lambda>a. [:a:]) P) * det (map_mat (\<lambda>a. [:a:]) Q) * det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) B)
[PROOF STEP]
by (simp add: ac_simps)
[PROOF STATE]
proof (state)
this:
det (map_mat (\<lambda>a. [:a:]) P) * det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) B) * det (map_mat (\<lambda>a. [:a:]) Q) = det (map_mat (\<lambda>a. [:a:]) P) * det (map_mat (\<lambda>a. [:a:]) Q) * det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) B)

goal (1 subgoal):
 1. char_poly A = char_poly B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
det (map_mat (\<lambda>a. [:a:]) P) * det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) B) * det (map_mat (\<lambda>a. [:a:]) Q) = det (map_mat (\<lambda>a. [:a:]) P) * det (map_mat (\<lambda>a. [:a:]) Q) * det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) B)

goal (1 subgoal):
 1. char_poly A = char_poly B
[PROOF STEP]
have "det (?XI + ?B) = char_poly B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) B) = char_poly B
[PROOF STEP]
unfolding char_poly_defs dim
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) B) = det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) B)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) B) = char_poly B

goal (1 subgoal):
 1. char_poly A = char_poly B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) B) = char_poly B

goal (1 subgoal):
 1. char_poly A = char_poly B
[PROOF STEP]
have "det ?P * det ?Q = det (?P * ?Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (map_mat (\<lambda>a. [:a:]) P) * det (map_mat (\<lambda>a. [:a:]) Q) = det (map_mat (\<lambda>a. [:a:]) P * map_mat (\<lambda>a. [:a:]) Q)
[PROOF STEP]
by (rule det_mult[symmetric], insert P Q, auto)
[PROOF STATE]
proof (state)
this:
det (map_mat (\<lambda>a. [:a:]) P) * det (map_mat (\<lambda>a. [:a:]) Q) = det (map_mat (\<lambda>a. [:a:]) P * map_mat (\<lambda>a. [:a:]) Q)

goal (1 subgoal):
 1. char_poly A = char_poly B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
det (map_mat (\<lambda>a. [:a:]) P) * det (map_mat (\<lambda>a. [:a:]) Q) = det (map_mat (\<lambda>a. [:a:]) P * map_mat (\<lambda>a. [:a:]) Q)

goal (1 subgoal):
 1. char_poly A = char_poly B
[PROOF STEP]
have "?P * ?Q = ?I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_mat (\<lambda>a. [:a:]) P * map_mat (\<lambda>a. [:a:]) Q = map_mat (\<lambda>a. [:a:]) (1\<^sub>m n)
[PROOF STEP]
unfolding PQ[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_mat (\<lambda>a. [:a:]) P * map_mat (\<lambda>a. [:a:]) Q = map_mat (\<lambda>a. [:a:]) (P * Q)
[PROOF STEP]
by (rule map_poly_mult[symmetric, OF P Q])
[PROOF STATE]
proof (state)
this:
map_mat (\<lambda>a. [:a:]) P * map_mat (\<lambda>a. [:a:]) Q = map_mat (\<lambda>a. [:a:]) (1\<^sub>m n)

goal (1 subgoal):
 1. char_poly A = char_poly B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map_mat (\<lambda>a. [:a:]) P * map_mat (\<lambda>a. [:a:]) Q = map_mat (\<lambda>a. [:a:]) (1\<^sub>m n)

goal (1 subgoal):
 1. char_poly A = char_poly B
[PROOF STEP]
have "det \<dots> = prod_list (diag_mat ?I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (map_mat (\<lambda>a. [:a:]) (1\<^sub>m n)) = prod_list (diag_mat (map_mat (\<lambda>a. [:a:]) (1\<^sub>m n)))
[PROOF STEP]
by (rule det_upper_triangular[of _ n], auto)
[PROOF STATE]
proof (state)
this:
det (map_mat (\<lambda>a. [:a:]) (1\<^sub>m n)) = prod_list (diag_mat (map_mat (\<lambda>a. [:a:]) (1\<^sub>m n)))

goal (1 subgoal):
 1. char_poly A = char_poly B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
det (map_mat (\<lambda>a. [:a:]) (1\<^sub>m n)) = prod_list (diag_mat (map_mat (\<lambda>a. [:a:]) (1\<^sub>m n)))

goal (1 subgoal):
 1. char_poly A = char_poly B
[PROOF STEP]
have "\<dots> = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod_list (diag_mat (map_mat (\<lambda>a. [:a:]) (1\<^sub>m n))) = 1
[PROOF STEP]
unfolding prod_list_diag_prod
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>i = 0..<dim_row (map_mat (\<lambda>a. [:a:]) (1\<^sub>m n)). map_mat (\<lambda>a. [:a:]) (1\<^sub>m n) $$ (i, i)) = 1
[PROOF STEP]
by (rule prod.neutral) simp
[PROOF STATE]
proof (state)
this:
prod_list (diag_mat (map_mat (\<lambda>a. [:a:]) (1\<^sub>m n))) = 1

goal (1 subgoal):
 1. char_poly A = char_poly B
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
char_poly A = 1 * char_poly B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
char_poly A = 1 * char_poly B

goal (1 subgoal):
 1. char_poly A = char_poly B
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
char_poly A = char_poly B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma degree_signof_mult[simp]: "degree (signof p * q) = degree q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (of_int (sign p) * q) = degree q
[PROOF STEP]
by (cases p rule: sign_cases) simp_all


[STATEMENT]
lemma degree_monic_char_poly: assumes A: "A \<in> carrier_mat n n"
  shows "degree (char_poly A) = n \<and> coeff (char_poly A) n = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (char_poly A) = n \<and> coeff (char_poly A) n = (1::'a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. degree (char_poly A) = n \<and> coeff (char_poly A) n = (1::'a)
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
A \<in> carrier_mat n n
[PROOF STEP]
have A': "[:0, 1:] \<cdot>\<^sub>m 1\<^sub>m (dim_row A) + map_mat (\<lambda>a. [:- a:]) A \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n

goal (1 subgoal):
 1. [:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row A) + map_mat (\<lambda>a. [:- a:]) A \<in> carrier_mat n n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row A) + map_mat (\<lambda>a. [:- a:]) A \<in> carrier_mat n n

goal (1 subgoal):
 1. degree (char_poly A) = n \<and> coeff (char_poly A) n = (1::'a)
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
A \<in> carrier_mat n n
[PROOF STEP]
have dA: "dim_row A = n"
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n

goal (1 subgoal):
 1. dim_row A = n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dim_row A = n

goal (1 subgoal):
 1. degree (char_poly A) = n \<and> coeff (char_poly A) n = (1::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (char_poly A) = n \<and> coeff (char_poly A) n = (1::'a)
[PROOF STEP]
unfolding char_poly_defs det_def'[OF A']
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (\<Sum>p | p permutes {0..<n}. of_int (sign p) * (\<Prod>i = 0..<n. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row A) + map_mat (\<lambda>a. [:- a:]) A) $$ (i, p i))) = n \<and> coeff (\<Sum>p | p permutes {0..<n}. of_int (sign p) * (\<Prod>i = 0..<n. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row A) + map_mat (\<lambda>a. [:- a:]) A) $$ (i, p i))) n = (1::'a)
[PROOF STEP]
proof (rule degree_lcoeff_sum[of _ id], auto simp: finite_permutations permutes_id dA)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. degree (\<Prod>i = 0..<n. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (i, i)) = n
 2. \<And>p. \<lbrakk>p permutes {0..<n}; p \<noteq> id\<rbrakk> \<Longrightarrow> degree (\<Prod>i = 0..<n. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (i, p i)) < n
 3. coeff (\<Prod>i = 0..<n. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (i, i)) n = (1::'a)
[PROOF STEP]
have both: "degree (\<Prod>i = 0..<n. ([:0, 1:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (i, i)) = n \<and>
      coeff (\<Prod>i = 0..<n. ([:0, 1:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (i, i)) n = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (\<Prod>i = 0..<n. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (i, i)) = n \<and> coeff (\<Prod>i = 0..<n. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (i, i)) n = (1::'a)
[PROOF STEP]
by (rule degree_prod_monic, insert A, auto)
[PROOF STATE]
proof (state)
this:
degree (\<Prod>i = 0..<n. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (i, i)) = n \<and> coeff (\<Prod>i = 0..<n. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (i, i)) n = (1::'a)

goal (3 subgoals):
 1. degree (\<Prod>i = 0..<n. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (i, i)) = n
 2. \<And>p. \<lbrakk>p permutes {0..<n}; p \<noteq> id\<rbrakk> \<Longrightarrow> degree (\<Prod>i = 0..<n. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (i, p i)) < n
 3. coeff (\<Prod>i = 0..<n. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (i, i)) n = (1::'a)
[PROOF STEP]
from both
[PROOF STATE]
proof (chain)
picking this:
degree (\<Prod>i = 0..<n. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (i, i)) = n \<and> coeff (\<Prod>i = 0..<n. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (i, i)) n = (1::'a)
[PROOF STEP]
show "degree (\<Prod>i = 0..<n. ([:0, 1:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (i, i)) = n"
[PROOF STATE]
proof (prove)
using this:
degree (\<Prod>i = 0..<n. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (i, i)) = n \<and> coeff (\<Prod>i = 0..<n. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (i, i)) n = (1::'a)

goal (1 subgoal):
 1. degree (\<Prod>i = 0..<n. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (i, i)) = n
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
degree (\<Prod>i = 0..<n. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (i, i)) = n

goal (2 subgoals):
 1. \<And>p. \<lbrakk>p permutes {0..<n}; p \<noteq> id\<rbrakk> \<Longrightarrow> degree (\<Prod>i = 0..<n. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (i, p i)) < n
 2. coeff (\<Prod>i = 0..<n. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (i, i)) n = (1::'a)
[PROOF STEP]
from both
[PROOF STATE]
proof (chain)
picking this:
degree (\<Prod>i = 0..<n. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (i, i)) = n \<and> coeff (\<Prod>i = 0..<n. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (i, i)) n = (1::'a)
[PROOF STEP]
show "coeff (\<Prod>i = 0..<n. ([:0, 1:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (i, i)) n = 1"
[PROOF STATE]
proof (prove)
using this:
degree (\<Prod>i = 0..<n. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (i, i)) = n \<and> coeff (\<Prod>i = 0..<n. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (i, i)) n = (1::'a)

goal (1 subgoal):
 1. coeff (\<Prod>i = 0..<n. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (i, i)) n = (1::'a)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
coeff (\<Prod>i = 0..<n. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (i, i)) n = (1::'a)

goal (1 subgoal):
 1. \<And>p. \<lbrakk>p permutes {0..<n}; p \<noteq> id\<rbrakk> \<Longrightarrow> degree (\<Prod>i = 0..<n. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (i, p i)) < n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>p permutes {0..<n}; p \<noteq> id\<rbrakk> \<Longrightarrow> degree (\<Prod>i = 0..<n. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (i, p i)) < n
[PROOF STEP]
fix p
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>p permutes {0..<n}; p \<noteq> id\<rbrakk> \<Longrightarrow> degree (\<Prod>i = 0..<n. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (i, p i)) < n
[PROOF STEP]
assume p: "p permutes {0..<n}"
      and "p \<noteq> id"
[PROOF STATE]
proof (state)
this:
p permutes {0..<n}
p \<noteq> id

goal (1 subgoal):
 1. \<And>p. \<lbrakk>p permutes {0..<n}; p \<noteq> id\<rbrakk> \<Longrightarrow> degree (\<Prod>i = 0..<n. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (i, p i)) < n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p permutes {0..<n}
p \<noteq> id
[PROOF STEP]
obtain i where i: "i < n" and pi: "p i \<noteq> i"
[PROOF STATE]
proof (prove)
using this:
p permutes {0..<n}
p \<noteq> id

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i < n; p i \<noteq> i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis atLeastLessThan_iff order_refl permutes_natset_le)
[PROOF STATE]
proof (state)
this:
i < n
p i \<noteq> i

goal (1 subgoal):
 1. \<And>p. \<lbrakk>p permutes {0..<n}; p \<noteq> id\<rbrakk> \<Longrightarrow> degree (\<Prod>i = 0..<n. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (i, p i)) < n
[PROOF STEP]
show "degree (\<Prod>i = 0..<n. ([:0, 1:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (i, p i)) < n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (\<Prod>i = 0..<n. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (i, p i)) < n
[PROOF STEP]
by (rule degree_prod_sum_lt_n[OF _ i], insert p i pi A, auto)
[PROOF STATE]
proof (state)
this:
degree (\<Prod>i = 0..<n. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (i, p i)) < n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
degree (char_poly A) = n \<and> coeff (char_poly A) n = (1::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma char_poly_factorized: fixes A :: "complex mat"
  assumes A: "A \<in> carrier_mat n n"
  shows "\<exists> as. char_poly A = (\<Prod> a \<leftarrow> as. [:- a, 1:]) \<and> length as = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>as. char_poly A = (\<Prod>a\<leftarrow>as. [:- a, 1:]) \<and> length as = n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>as. char_poly A = (\<Prod>a\<leftarrow>as. [:- a, 1:]) \<and> length as = n
[PROOF STEP]
let ?p = "char_poly A"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>as. char_poly A = (\<Prod>a\<leftarrow>as. [:- a, 1:]) \<and> length as = n
[PROOF STEP]
from fundamental_theorem_algebra_factorized[of ?p]
[PROOF STATE]
proof (chain)
picking this:
\<exists>as. Polynomial.smult (lead_coeff (char_poly A)) (\<Prod>a\<leftarrow>as. [:- a, 1:]) = char_poly A \<and> length as = degree (char_poly A)
[PROOF STEP]
obtain as
  where "Polynomial.smult (coeff ?p (degree ?p)) (\<Prod>a\<leftarrow>as. [:- a, 1:]) = ?p"
[PROOF STATE]
proof (prove)
using this:
\<exists>as. Polynomial.smult (lead_coeff (char_poly A)) (\<Prod>a\<leftarrow>as. [:- a, 1:]) = char_poly A \<and> length as = degree (char_poly A)

goal (1 subgoal):
 1. (\<And>as. Polynomial.smult (lead_coeff (char_poly A)) (\<Prod>a\<leftarrow>as. [:- a, 1:]) = char_poly A \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Polynomial.smult (lead_coeff (char_poly A)) (\<Prod>a\<leftarrow>as. [:- a, 1:]) = char_poly A

goal (1 subgoal):
 1. \<exists>as. char_poly A = (\<Prod>a\<leftarrow>as. [:- a, 1:]) \<and> length as = n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Polynomial.smult (lead_coeff (char_poly A)) (\<Prod>a\<leftarrow>as. [:- a, 1:]) = char_poly A

goal (1 subgoal):
 1. \<exists>as. char_poly A = (\<Prod>a\<leftarrow>as. [:- a, 1:]) \<and> length as = n
[PROOF STEP]
have "coeff ?p (degree ?p) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monic (char_poly A)
[PROOF STEP]
using degree_monic_char_poly[OF A]
[PROOF STATE]
proof (prove)
using this:
degree (char_poly A) = n \<and> coeff (char_poly A) n = 1

goal (1 subgoal):
 1. monic (char_poly A)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
monic (char_poly A)

goal (1 subgoal):
 1. \<exists>as. char_poly A = (\<Prod>a\<leftarrow>as. [:- a, 1:]) \<and> length as = n
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Polynomial.smult 1 (\<Prod>a\<leftarrow>as. [:- a, 1:]) = char_poly A
[PROOF STEP]
have cA: "?p = (\<Prod>a\<leftarrow>as. [:- a, 1:])"
[PROOF STATE]
proof (prove)
using this:
Polynomial.smult 1 (\<Prod>a\<leftarrow>as. [:- a, 1:]) = char_poly A

goal (1 subgoal):
 1. char_poly A = (\<Prod>a\<leftarrow>as. [:- a, 1:])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
char_poly A = (\<Prod>a\<leftarrow>as. [:- a, 1:])

goal (1 subgoal):
 1. \<exists>as. char_poly A = (\<Prod>a\<leftarrow>as. [:- a, 1:]) \<and> length as = n
[PROOF STEP]
from degree_monic_char_poly[OF A]
[PROOF STATE]
proof (chain)
picking this:
degree (char_poly A) = n \<and> coeff (char_poly A) n = 1
[PROOF STEP]
have "degree ?p = n"
[PROOF STATE]
proof (prove)
using this:
degree (char_poly A) = n \<and> coeff (char_poly A) n = 1

goal (1 subgoal):
 1. degree (char_poly A) = n
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
degree (char_poly A) = n

goal (1 subgoal):
 1. \<exists>as. char_poly A = (\<Prod>a\<leftarrow>as. [:- a, 1:]) \<and> length as = n
[PROOF STEP]
with degree_linear_factors[of uminus as, folded cA]
[PROOF STATE]
proof (chain)
picking this:
degree (char_poly A) = length as
degree (char_poly A) = n
[PROOF STEP]
have "length as = n"
[PROOF STATE]
proof (prove)
using this:
degree (char_poly A) = length as
degree (char_poly A) = n

goal (1 subgoal):
 1. length as = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length as = n

goal (1 subgoal):
 1. \<exists>as. char_poly A = (\<Prod>a\<leftarrow>as. [:- a, 1:]) \<and> length as = n
[PROOF STEP]
with cA
[PROOF STATE]
proof (chain)
picking this:
char_poly A = (\<Prod>a\<leftarrow>as. [:- a, 1:])
length as = n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
char_poly A = (\<Prod>a\<leftarrow>as. [:- a, 1:])
length as = n

goal (1 subgoal):
 1. \<exists>as. char_poly A = (\<Prod>a\<leftarrow>as. [:- a, 1:]) \<and> length as = n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>as. char_poly A = (\<Prod>a\<leftarrow>as. [:- a, 1:]) \<and> length as = n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma char_poly_four_block_zeros_col: assumes A1: "A1 \<in> carrier_mat 1 1"
  and A2: "A2 \<in> carrier_mat 1 n" and A3: "A3 \<in> carrier_mat n n"
  shows "char_poly (four_block_mat A1 A2 (0\<^sub>m n 1) A3) = char_poly A1 * char_poly A3"
    (is "char_poly ?A = ?cp1 * ?cp3")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. char_poly (four_block_mat A1 A2 (0\<^sub>m n 1) A3) = char_poly A1 * char_poly A3
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. char_poly (four_block_mat A1 A2 (0\<^sub>m n 1) A3) = char_poly A1 * char_poly A3
[PROOF STEP]
let ?cm = "\<lambda> A. [:0, 1:] \<cdot>\<^sub>m 1\<^sub>m (dim_row A) +
         map_mat (\<lambda>a. [:- a:]) A"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. char_poly (four_block_mat A1 A2 (0\<^sub>m n 1) A3) = char_poly A1 * char_poly A3
[PROOF STEP]
let ?B2 = "map_mat (\<lambda>a. [:- a:]) A2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. char_poly (four_block_mat A1 A2 (0\<^sub>m n 1) A3) = char_poly A1 * char_poly A3
[PROOF STEP]
have "char_poly ?A = det (?cm ?A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. char_poly (four_block_mat A1 A2 (0\<^sub>m n 1) A3) = det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row (four_block_mat A1 A2 (0\<^sub>m n 1) A3)) + map_mat (\<lambda>a. [:- a:]) (four_block_mat A1 A2 (0\<^sub>m n 1) A3))
[PROOF STEP]
unfolding char_poly_defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row (four_block_mat A1 A2 (0\<^sub>m n 1) A3)) + map_mat (\<lambda>a. [:- a:]) (four_block_mat A1 A2 (0\<^sub>m n 1) A3)) = det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row (four_block_mat A1 A2 (0\<^sub>m n 1) A3)) + map_mat (\<lambda>a. [:- a:]) (four_block_mat A1 A2 (0\<^sub>m n 1) A3))
[PROOF STEP]
using A1 A3
[PROOF STATE]
proof (prove)
using this:
A1 \<in> carrier_mat 1 1
A3 \<in> carrier_mat n n

goal (1 subgoal):
 1. det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row (four_block_mat A1 A2 (0\<^sub>m n 1) A3)) + map_mat (\<lambda>a. [:- a:]) (four_block_mat A1 A2 (0\<^sub>m n 1) A3)) = det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row (four_block_mat A1 A2 (0\<^sub>m n 1) A3)) + map_mat (\<lambda>a. [:- a:]) (four_block_mat A1 A2 (0\<^sub>m n 1) A3))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
char_poly (four_block_mat A1 A2 (0\<^sub>m n 1) A3) = det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row (four_block_mat A1 A2 (0\<^sub>m n 1) A3)) + map_mat (\<lambda>a. [:- a:]) (four_block_mat A1 A2 (0\<^sub>m n 1) A3))

goal (1 subgoal):
 1. char_poly (four_block_mat A1 A2 (0\<^sub>m n 1) A3) = char_poly A1 * char_poly A3
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
char_poly (four_block_mat A1 A2 (0\<^sub>m n 1) A3) = det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row (four_block_mat A1 A2 (0\<^sub>m n 1) A3)) + map_mat (\<lambda>a. [:- a:]) (four_block_mat A1 A2 (0\<^sub>m n 1) A3))

goal (1 subgoal):
 1. char_poly (four_block_mat A1 A2 (0\<^sub>m n 1) A3) = char_poly A1 * char_poly A3
[PROOF STEP]
have "?cm ?A = four_block_mat (?cm A1) ?B2 (0\<^sub>m n 1) (?cm A3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row (four_block_mat A1 A2 (0\<^sub>m n 1) A3)) + map_mat (\<lambda>a. [:- a:]) (four_block_mat A1 A2 (0\<^sub>m n 1) A3) = four_block_mat ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row A1) + map_mat (\<lambda>a. [:- a:]) A1) (map_mat (\<lambda>a. [:- a:]) A2) (0\<^sub>m n 1) ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row A3) + map_mat (\<lambda>a. [:- a:]) A3)
[PROOF STEP]
by (rule eq_matI, insert A1 A2 A3, auto simp: one_poly_def)
[PROOF STATE]
proof (state)
this:
[:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row (four_block_mat A1 A2 (0\<^sub>m n 1) A3)) + map_mat (\<lambda>a. [:- a:]) (four_block_mat A1 A2 (0\<^sub>m n 1) A3) = four_block_mat ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row A1) + map_mat (\<lambda>a. [:- a:]) A1) (map_mat (\<lambda>a. [:- a:]) A2) (0\<^sub>m n 1) ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row A3) + map_mat (\<lambda>a. [:- a:]) A3)

goal (1 subgoal):
 1. char_poly (four_block_mat A1 A2 (0\<^sub>m n 1) A3) = char_poly A1 * char_poly A3
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
[:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row (four_block_mat A1 A2 (0\<^sub>m n 1) A3)) + map_mat (\<lambda>a. [:- a:]) (four_block_mat A1 A2 (0\<^sub>m n 1) A3) = four_block_mat ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row A1) + map_mat (\<lambda>a. [:- a:]) A1) (map_mat (\<lambda>a. [:- a:]) A2) (0\<^sub>m n 1) ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row A3) + map_mat (\<lambda>a. [:- a:]) A3)

goal (1 subgoal):
 1. char_poly (four_block_mat A1 A2 (0\<^sub>m n 1) A3) = char_poly A1 * char_poly A3
[PROOF STEP]
have "det \<dots> = det (?cm A1) * det (?cm A3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (four_block_mat ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row A1) + map_mat (\<lambda>a. [:- a:]) A1) (map_mat (\<lambda>a. [:- a:]) A2) (0\<^sub>m n 1) ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row A3) + map_mat (\<lambda>a. [:- a:]) A3)) = det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row A1) + map_mat (\<lambda>a. [:- a:]) A1) * det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row A3) + map_mat (\<lambda>a. [:- a:]) A3)
[PROOF STEP]
by (rule det_four_block_mat_lower_left_zero_col[OF _ _ refl], insert A1 A2 A3, auto)
[PROOF STATE]
proof (state)
this:
det (four_block_mat ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row A1) + map_mat (\<lambda>a. [:- a:]) A1) (map_mat (\<lambda>a. [:- a:]) A2) (0\<^sub>m n 1) ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row A3) + map_mat (\<lambda>a. [:- a:]) A3)) = det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row A1) + map_mat (\<lambda>a. [:- a:]) A1) * det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row A3) + map_mat (\<lambda>a. [:- a:]) A3)

goal (1 subgoal):
 1. char_poly (four_block_mat A1 A2 (0\<^sub>m n 1) A3) = char_poly A1 * char_poly A3
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
det (four_block_mat ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row A1) + map_mat (\<lambda>a. [:- a:]) A1) (map_mat (\<lambda>a. [:- a:]) A2) (0\<^sub>m n 1) ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row A3) + map_mat (\<lambda>a. [:- a:]) A3)) = det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row A1) + map_mat (\<lambda>a. [:- a:]) A1) * det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row A3) + map_mat (\<lambda>a. [:- a:]) A3)

goal (1 subgoal):
 1. char_poly (four_block_mat A1 A2 (0\<^sub>m n 1) A3) = char_poly A1 * char_poly A3
[PROOF STEP]
have "\<dots> = ?cp1 * ?cp3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row A1) + map_mat (\<lambda>a. [:- a:]) A1) * det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row A3) + map_mat (\<lambda>a. [:- a:]) A3) = char_poly A1 * char_poly A3
[PROOF STEP]
unfolding char_poly_defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row A1) + map_mat (\<lambda>a. [:- a:]) A1) * det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row A3) + map_mat (\<lambda>a. [:- a:]) A3) = det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row A1) + map_mat (\<lambda>a. [:- a:]) A1) * det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row A3) + map_mat (\<lambda>a. [:- a:]) A3)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row A1) + map_mat (\<lambda>a. [:- a:]) A1) * det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row A3) + map_mat (\<lambda>a. [:- a:]) A3) = char_poly A1 * char_poly A3

goal (1 subgoal):
 1. char_poly (four_block_mat A1 A2 (0\<^sub>m n 1) A3) = char_poly A1 * char_poly A3
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
char_poly (four_block_mat A1 A2 (0\<^sub>m n 1) A3) = char_poly A1 * char_poly A3
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
char_poly (four_block_mat A1 A2 (0\<^sub>m n 1) A3) = char_poly A1 * char_poly A3

goal (1 subgoal):
 1. char_poly (four_block_mat A1 A2 (0\<^sub>m n 1) A3) = char_poly A1 * char_poly A3
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
char_poly (four_block_mat A1 A2 (0\<^sub>m n 1) A3) = char_poly A1 * char_poly A3

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma char_poly_transpose_mat[simp]: assumes A: "A \<in> carrier_mat n n"
  shows "char_poly (transpose_mat A) = char_poly A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. char_poly A\<^sup>T = char_poly A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. char_poly A\<^sup>T = char_poly A
[PROOF STEP]
let ?A = "[:0, 1:] \<cdot>\<^sub>m 1\<^sub>m (dim_row A) + map_mat (\<lambda>a. [:- a:]) A"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. char_poly A\<^sup>T = char_poly A
[PROOF STEP]
have A': "?A \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row A) + map_mat (\<lambda>a. [:- a:]) A \<in> carrier_mat n n
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n

goal (1 subgoal):
 1. [:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row A) + map_mat (\<lambda>a. [:- a:]) A \<in> carrier_mat n n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row A) + map_mat (\<lambda>a. [:- a:]) A \<in> carrier_mat n n

goal (1 subgoal):
 1. char_poly A\<^sup>T = char_poly A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. char_poly A\<^sup>T = char_poly A
[PROOF STEP]
unfolding char_poly_defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row A\<^sup>T) + map_mat (\<lambda>a. [:- a:]) A\<^sup>T) = det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row A) + map_mat (\<lambda>a. [:- a:]) A)
[PROOF STEP]
by (subst det_transpose[symmetric, OF A'], rule arg_cong[of _ _ det],
    insert A, auto)
[PROOF STATE]
proof (state)
this:
char_poly A\<^sup>T = char_poly A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pderiv_char_poly: fixes A :: "'a :: idom mat"
  assumes A: "A \<in> carrier_mat n n"
  shows "pderiv (char_poly A) = (\<Sum>i < n. char_poly (mat_delete A i i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
let ?det = Determinant.det
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
let ?m = "map_mat (\<lambda>a. [:- a:])"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
let ?lam = "[:0, 1:] \<cdot>\<^sub>m 1\<^sub>m n :: 'a poly mat"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
A \<in> carrier_mat n n
[PROOF STEP]
have id: "dim_row A = n"
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n

goal (1 subgoal):
 1. dim_row A = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dim_row A = n

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
define mA where "mA = ?m A"
[PROOF STATE]
proof (state)
this:
mA = map_mat (\<lambda>a. [:- a:]) A

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
define lam where "lam = ?lam"
[PROOF STATE]
proof (state)
this:
lam = [:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
let ?sum = "lam + mA"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
define Sum where "Sum = ?sum"
[PROOF STATE]
proof (state)
this:
Sum = lam + mA

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
have mA: "mA \<in> carrier_mat n n" and
    lam: "lam \<in> carrier_mat n n" and
    Sum: "Sum \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mA \<in> carrier_mat n n &&& lam \<in> carrier_mat n n &&& Sum \<in> carrier_mat n n
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n

goal (1 subgoal):
 1. mA \<in> carrier_mat n n &&& lam \<in> carrier_mat n n &&& Sum \<in> carrier_mat n n
[PROOF STEP]
unfolding mA_def Sum_def lam_def
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n

goal (1 subgoal):
 1. map_mat (\<lambda>a. [:- a:]) A \<in> carrier_mat n n &&& [:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n \<in> carrier_mat n n &&& [:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A \<in> carrier_mat n n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mA \<in> carrier_mat n n
lam \<in> carrier_mat n n
Sum \<in> carrier_mat n n

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
let ?P = "{p. p permutes {0..<n}}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
let ?e = "\<lambda> p. (\<Prod>i = 0..<n. Sum $$ (i, p i))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
let ?f = "\<lambda> p a. signof p * (\<Prod>i\<in>{0..<n} - {a}. Sum $$ (i, p i)) * pderiv (Sum $$ (a, p a))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
let ?g = "\<lambda> p a. signof p * (\<Prod>i\<in>{0..<n} - {a}. Sum $$ (i, p i))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
define f where "f = ?f"
[PROOF STATE]
proof (state)
this:
f = (\<lambda>p a. of_int (sign p) * (\<Prod>i\<in>{0..<n} - {a}. Sum $$ (i, p i)) * pderiv (Sum $$ (a, p a)))

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
define g where "g = ?g"
[PROOF STATE]
proof (state)
this:
g = (\<lambda>p a. of_int (sign p) * (\<Prod>i\<in>{0..<n} - {a}. Sum $$ (i, p i)))

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
g = (\<lambda>p a. of_int (sign p) * (\<Prod>i\<in>{0..<n} - {a}. Sum $$ (i, p i)))

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
fix p
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
assume p: "p permutes {0 ..< n}"
[PROOF STATE]
proof (state)
this:
p permutes {0..<n}

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
have "pderiv (signof p :: 'a poly) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pderiv (of_int (sign p)) = 0
[PROOF STEP]
by (cases p rule: sign_cases) (simp_all add: pderiv_minus)
[PROOF STATE]
proof (state)
this:
pderiv (of_int (sign p)) = 0

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
hence "pderiv (signof p * ?e p) = signof p * pderiv (\<Prod>i = 0..<n. Sum $$ (i, p i))"
[PROOF STATE]
proof (prove)
using this:
pderiv (of_int (sign p)) = 0

goal (1 subgoal):
 1. pderiv (of_int (sign p) * (\<Prod>i = 0..<n. Sum $$ (i, p i))) = of_int (sign p) * pderiv (\<Prod>i = 0..<n. Sum $$ (i, p i))
[PROOF STEP]
unfolding pderiv_mult
[PROOF STATE]
proof (prove)
using this:
pderiv (of_int (sign p)) = 0

goal (1 subgoal):
 1. of_int (sign p) * pderiv (\<Prod>i = 0..<n. Sum $$ (i, p i)) + (\<Prod>i = 0..<n. Sum $$ (i, p i)) * pderiv (of_int (sign p)) = of_int (sign p) * pderiv (\<Prod>i = 0..<n. Sum $$ (i, p i))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pderiv (of_int (sign p) * (\<Prod>i = 0..<n. Sum $$ (i, p i))) = of_int (sign p) * pderiv (\<Prod>i = 0..<n. Sum $$ (i, p i))

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
pderiv (of_int (sign p) * (\<Prod>i = 0..<n. Sum $$ (i, p i))) = of_int (sign p) * pderiv (\<Prod>i = 0..<n. Sum $$ (i, p i))

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
have "signof p * pderiv (\<Prod>i = 0..<n. Sum $$ (i, p i)) =
       (\<Sum>a = 0..<n. f p a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int (sign p) * pderiv (\<Prod>i = 0..<n. Sum $$ (i, p i)) = sum (f p) {0..<n}
[PROOF STEP]
unfolding pderiv_prod sum_distrib_left f_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>na = 0..<n. of_int (sign p) * ((\<Prod>i\<in>{0..<n} - {na}. Sum $$ (i, p i)) * pderiv (Sum $$ (na, p na)))) = (\<Sum>a = 0..<n. of_int (sign p) * (\<Prod>i\<in>{0..<n} - {a}. Sum $$ (i, p i)) * pderiv (Sum $$ (a, p a)))
[PROOF STEP]
by (simp add: ac_simps)
[PROOF STATE]
proof (state)
this:
of_int (sign p) * pderiv (\<Prod>i = 0..<n. Sum $$ (i, p i)) = sum (f p) {0..<n}

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
of_int (sign p) * pderiv (\<Prod>i = 0..<n. Sum $$ (i, p i)) = sum (f p) {0..<n}

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
note calculation
[PROOF STATE]
proof (state)
this:
pderiv (of_int (sign p) * (\<Prod>i = 0..<n. Sum $$ (i, p i))) = sum (f p) {0..<n}

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?p4 permutes {0..<n} \<Longrightarrow> pderiv (of_int (sign ?p4) * (\<Prod>i = 0..<n. Sum $$ (i, ?p4 i))) = sum (f ?p4) {0..<n}

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
note to_f = this
[PROOF STATE]
proof (state)
this:
?p4 permutes {0..<n} \<Longrightarrow> pderiv (of_int (sign ?p4) * (\<Prod>i = 0..<n. Sum $$ (i, ?p4 i))) = sum (f ?p4) {0..<n}

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?p4 permutes {0..<n} \<Longrightarrow> pderiv (of_int (sign ?p4) * (\<Prod>i = 0..<n. Sum $$ (i, ?p4 i))) = sum (f ?p4) {0..<n}

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
assume a: "a < n"
[PROOF STATE]
proof (state)
this:
a < n

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
have Psplit: "?P = {p. p permutes {0..<n} \<and> p a = a} \<union> (?P - {p. p a = a})" (is "_ = ?Pa \<union> ?Pz")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {p. p permutes {0..<n}} = {p. p permutes {0..<n} \<and> p a = a} \<union> ({p. p permutes {0..<n}} - {p. p a = a})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{p. p permutes {0..<n}} = {p. p permutes {0..<n} \<and> p a = a} \<union> ({p. p permutes {0..<n}} - {p. p a = a})

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
{p. p permutes {0..<n}} = {p. p permutes {0..<n} \<and> p a = a} \<union> ({p. p permutes {0..<n}} - {p. p a = a})

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
fix p
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
assume p: "p permutes {0 ..< n}" "p a \<noteq> a"
[PROOF STATE]
proof (state)
this:
p permutes {0..<n}
p a \<noteq> a

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
hence "pderiv (Sum $$ (a, p a)) = 0"
[PROOF STATE]
proof (prove)
using this:
p permutes {0..<n}
p a \<noteq> a

goal (1 subgoal):
 1. pderiv (Sum $$ (a, p a)) = 0
[PROOF STEP]
unfolding Sum_def lam_def mA_def
[PROOF STATE]
proof (prove)
using this:
p permutes {0..<n}
p a \<noteq> a

goal (1 subgoal):
 1. pderiv (([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (a, p a)) = 0
[PROOF STEP]
using a p A
[PROOF STATE]
proof (prove)
using this:
p permutes {0..<n}
p a \<noteq> a
a < n
p permutes {0..<n}
p a \<noteq> a
A \<in> carrier_mat n n

goal (1 subgoal):
 1. pderiv (([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (a, p a)) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pderiv (Sum $$ (a, p a)) = 0

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
hence "f p a = 0"
[PROOF STATE]
proof (prove)
using this:
pderiv (Sum $$ (a, p a)) = 0

goal (1 subgoal):
 1. f p a = 0
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
using this:
pderiv (Sum $$ (a, p a)) = 0

goal (1 subgoal):
 1. of_int (sign p) * (\<Prod>i\<in>{0..<n} - {a}. Sum $$ (i, p i)) * pderiv (Sum $$ (a, p a)) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f p a = 0

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?p4 permutes {0..<n}; ?p4 a \<noteq> a\<rbrakk> \<Longrightarrow> f ?p4 a = 0

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
note 0 = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>?p4 permutes {0..<n}; ?p4 a \<noteq> a\<rbrakk> \<Longrightarrow> f ?p4 a = 0

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>?p4 permutes {0..<n}; ?p4 a \<noteq> a\<rbrakk> \<Longrightarrow> f ?p4 a = 0

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
fix p
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
assume p: "p permutes {0 ..< n}" "p a = a"
[PROOF STATE]
proof (state)
this:
p permutes {0..<n}
p a = a

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
hence "pderiv (Sum $$ (a, p a)) = 1"
[PROOF STATE]
proof (prove)
using this:
p permutes {0..<n}
p a = a

goal (1 subgoal):
 1. pderiv (Sum $$ (a, p a)) = 1
[PROOF STEP]
unfolding Sum_def lam_def mA_def
[PROOF STATE]
proof (prove)
using this:
p permutes {0..<n}
p a = a

goal (1 subgoal):
 1. pderiv (([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (a, p a)) = 1
[PROOF STEP]
using a p A
[PROOF STATE]
proof (prove)
using this:
p permutes {0..<n}
p a = a
a < n
p permutes {0..<n}
p a = a
A \<in> carrier_mat n n

goal (1 subgoal):
 1. pderiv (([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (a, p a)) = 1
[PROOF STEP]
by (auto simp: pderiv_pCons)
[PROOF STATE]
proof (state)
this:
pderiv (Sum $$ (a, p a)) = 1

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
hence "f p a = g p a"
[PROOF STATE]
proof (prove)
using this:
pderiv (Sum $$ (a, p a)) = 1

goal (1 subgoal):
 1. f p a = g p a
[PROOF STEP]
unfolding f_def g_def
[PROOF STATE]
proof (prove)
using this:
pderiv (Sum $$ (a, p a)) = 1

goal (1 subgoal):
 1. of_int (sign p) * (\<Prod>i\<in>{0..<n} - {a}. Sum $$ (i, p i)) * pderiv (Sum $$ (a, p a)) = of_int (sign p) * (\<Prod>i\<in>{0..<n} - {a}. Sum $$ (i, p i))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f p a = g p a

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?p4 permutes {0..<n}; ?p4 a = a\<rbrakk> \<Longrightarrow> f ?p4 a = g ?p4 a

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
note fg = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>?p4 permutes {0..<n}; ?p4 a = a\<rbrakk> \<Longrightarrow> f ?p4 a = g ?p4 a

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
let ?n = "n - 1"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
from a
[PROOF STATE]
proof (chain)
picking this:
a < n
[PROOF STEP]
have n: "Suc ?n = n"
[PROOF STATE]
proof (prove)
using this:
a < n

goal (1 subgoal):
 1. Suc (n - 1) = n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Suc (n - 1) = n

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
let ?B = "[:0, 1:] \<cdot>\<^sub>m 1\<^sub>m ?n + ?m (mat_delete A a a)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
have B: "?B \<in> carrier_mat ?n ?n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a) \<in> carrier_mat (n - 1) (n - 1)
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n

goal (1 subgoal):
 1. [:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a) \<in> carrier_mat (n - 1) (n - 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a) \<in> carrier_mat (n - 1) (n - 1)

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
have "sum (\<lambda> p. f p a) ?P = sum (\<lambda> p. f p a) ?Pa + sum (\<lambda> p. f p a) ?Pz"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>p | p permutes {0..<n}. f p a) = (\<Sum>p | p permutes {0..<n} \<and> p a = a. f p a) + (\<Sum>p\<in>{p. p permutes {0..<n}} - {p. p a = a}. f p a)
[PROOF STEP]
by (subst sum.union_disjoint[symmetric], auto simp: finite_permutations Psplit[symmetric])
[PROOF STATE]
proof (state)
this:
(\<Sum>p | p permutes {0..<n}. f p a) = (\<Sum>p | p permutes {0..<n} \<and> p a = a. f p a) + (\<Sum>p\<in>{p. p permutes {0..<n}} - {p. p a = a}. f p a)

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>p | p permutes {0..<n}. f p a) = (\<Sum>p | p permutes {0..<n} \<and> p a = a. f p a) + (\<Sum>p\<in>{p. p permutes {0..<n}} - {p. p a = a}. f p a)

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
have "\<dots> = sum (\<lambda> p. f p a) ?Pa"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>p | p permutes {0..<n} \<and> p a = a. f p a) + (\<Sum>p\<in>{p. p permutes {0..<n}} - {p. p a = a}. f p a) = (\<Sum>p | p permutes {0..<n} \<and> p a = a. f p a)
[PROOF STEP]
by (subst (2) sum.neutral, insert 0, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>p | p permutes {0..<n} \<and> p a = a. f p a) + (\<Sum>p\<in>{p. p permutes {0..<n}} - {p. p a = a}. f p a) = (\<Sum>p | p permutes {0..<n} \<and> p a = a. f p a)

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>p | p permutes {0..<n} \<and> p a = a. f p a) + (\<Sum>p\<in>{p. p permutes {0..<n}} - {p. p a = a}. f p a) = (\<Sum>p | p permutes {0..<n} \<and> p a = a. f p a)

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
have "\<dots> = sum (\<lambda> p. g p a) ?Pa"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>p | p permutes {0..<n} \<and> p a = a. f p a) = (\<Sum>p | p permutes {0..<n} \<and> p a = a. g p a)
[PROOF STEP]
by (rule sum.cong, auto simp: fg)
[PROOF STATE]
proof (state)
this:
(\<Sum>p | p permutes {0..<n} \<and> p a = a. f p a) = (\<Sum>p | p permutes {0..<n} \<and> p a = a. g p a)

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>p | p permutes {0..<n} \<and> p a = a. f p a) = (\<Sum>p | p permutes {0..<n} \<and> p a = a. g p a)

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
have "\<dots> = ?det ?B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>p | p permutes {0..<n} \<and> p a = a. g p a) = det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a))
[PROOF STEP]
unfolding det_def'[OF B]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>p | p permutes {0..<n} \<and> p a = a. g p a) = (\<Sum>p | p permutes {0..<n - 1}. of_int (sign p) * (\<Prod>i = 0..<n - 1. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (i, p i)))
[PROOF STEP]
unfolding permutation_fix[of a ?n a, unfolded n, OF a a]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>p\<in>permutation_insert a a ` {q. q permutes {0..<n - 1}}. g p a) = (\<Sum>p | p permutes {0..<n - 1}. of_int (sign p) * (\<Prod>i = 0..<n - 1. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (i, p i)))
[PROOF STEP]
unfolding sum.reindex[OF permutation_insert_inj_on[of a ?n a, unfolded n, OF a a]] o_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>{q. q permutes {0..<n - 1}}. g (permutation_insert a a x) a) = (\<Sum>p | p permutes {0..<n - 1}. of_int (sign p) * (\<Prod>i = 0..<n - 1. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (i, p i)))
[PROOF STEP]
proof (rule sum.cong[OF refl])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {q. q permutes {0..<n - 1}} \<Longrightarrow> g (permutation_insert a a x) a = of_int (sign x) * (\<Prod>i = 0..<n - 1. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (i, x i))
[PROOF STEP]
fix p
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {q. q permutes {0..<n - 1}} \<Longrightarrow> g (permutation_insert a a x) a = of_int (sign x) * (\<Prod>i = 0..<n - 1. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (i, x i))
[PROOF STEP]
let ?Q = "{p. p permutes {0..<?n}}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {q. q permutes {0..<n - 1}} \<Longrightarrow> g (permutation_insert a a x) a = of_int (sign x) * (\<Prod>i = 0..<n - 1. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (i, x i))
[PROOF STEP]
assume "p \<in> ?Q"
[PROOF STATE]
proof (state)
this:
p \<in> {p. p permutes {0..<n - 1}}

goal (1 subgoal):
 1. \<And>x. x \<in> {q. q permutes {0..<n - 1}} \<Longrightarrow> g (permutation_insert a a x) a = of_int (sign x) * (\<Prod>i = 0..<n - 1. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (i, x i))
[PROOF STEP]
hence p: "p permutes {0 ..< ?n}"
[PROOF STATE]
proof (prove)
using this:
p \<in> {p. p permutes {0..<n - 1}}

goal (1 subgoal):
 1. p permutes {0..<n - 1}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p permutes {0..<n - 1}

goal (1 subgoal):
 1. \<And>x. x \<in> {q. q permutes {0..<n - 1}} \<Longrightarrow> g (permutation_insert a a x) a = of_int (sign x) * (\<Prod>i = 0..<n - 1. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (i, x i))
[PROOF STEP]
let ?p = "permutation_insert a a p"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {q. q permutes {0..<n - 1}} \<Longrightarrow> g (permutation_insert a a x) a = of_int (sign x) * (\<Prod>i = 0..<n - 1. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (i, x i))
[PROOF STEP]
let ?i = "insert_index a"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {q. q permutes {0..<n - 1}} \<Longrightarrow> g (permutation_insert a a x) a = of_int (sign x) * (\<Prod>i = 0..<n - 1. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (i, x i))
[PROOF STEP]
have sign: "signof ?p = signof p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int (sign (permutation_insert a a p)) = of_int (sign p)
[PROOF STEP]
unfolding signof_permutation_insert[OF p, unfolded n, OF a a]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- (1::'b)) ^ (a + a) * of_int (sign p) = of_int (sign p)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
of_int (sign (permutation_insert a a p)) = of_int (sign p)

goal (1 subgoal):
 1. \<And>x. x \<in> {q. q permutes {0..<n - 1}} \<Longrightarrow> g (permutation_insert a a x) a = of_int (sign x) * (\<Prod>i = 0..<n - 1. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (i, x i))
[PROOF STEP]
show "g (permutation_insert a a p) a = signof p * (\<Prod>i = 0..<?n. ?B $$ (i, p i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g (permutation_insert a a p) a = of_int (sign p) * (\<Prod>i = 0..<n - 1. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (i, p i))
[PROOF STEP]
unfolding g_def sign
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int (sign p) * (\<Prod>i\<in>{0..<n} - {a}. Sum $$ (i, permutation_insert a a p i)) = of_int (sign p) * (\<Prod>i = 0..<n - 1. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (i, p i))
[PROOF STEP]
proof (rule arg_cong[of _ _ "(*) (signof p)"])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Prod>i\<in>{0..<n} - {a}. Sum $$ (i, permutation_insert a a p i)) = (\<Prod>i = 0..<n - 1. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (i, p i))
[PROOF STEP]
have "(\<Prod>i\<in>{0..<n} - {a}. Sum $$ (i, ?p i)) =
           prod (($$) Sum) ((\<lambda>x. (x, ?p x)) ` ({0..<n} - {a}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>i\<in>{0..<n} - {a}. Sum $$ (i, permutation_insert a a p i)) = prod (($$) Sum) ((\<lambda>x. (x, permutation_insert a a p x)) ` ({0..<n} - {a}))
[PROOF STEP]
unfolding prod.reindex[OF inj_on_convol_ident, of _ ?p] o_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>i\<in>{0..<n} - {a}. Sum $$ (i, permutation_insert a a p i)) = (\<Prod>x\<in>{0..<n} - {a}. Sum $$ (x, permutation_insert a a p x))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(\<Prod>i\<in>{0..<n} - {a}. Sum $$ (i, permutation_insert a a p i)) = prod (($$) Sum) ((\<lambda>x. (x, permutation_insert a a p x)) ` ({0..<n} - {a}))

goal (1 subgoal):
 1. (\<Prod>i\<in>{0..<n} - {a}. Sum $$ (i, permutation_insert a a p i)) = (\<Prod>i = 0..<n - 1. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (i, p i))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Prod>i\<in>{0..<n} - {a}. Sum $$ (i, permutation_insert a a p i)) = prod (($$) Sum) ((\<lambda>x. (x, permutation_insert a a p x)) ` ({0..<n} - {a}))

goal (1 subgoal):
 1. (\<Prod>i\<in>{0..<n} - {a}. Sum $$ (i, permutation_insert a a p i)) = (\<Prod>i = 0..<n - 1. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (i, p i))
[PROOF STEP]
have "\<dots> = (\<Prod> ii \<in> {(i', ?p i') |i'. i' \<in> {0..<n} - {a}}. Sum $$ ii)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod (($$) Sum) ((\<lambda>x. (x, permutation_insert a a p x)) ` ({0..<n} - {a})) = prod (($$) Sum) {(i', permutation_insert a a p i') |i'. i' \<in> {0..<n} - {a}}
[PROOF STEP]
by (rule prod.cong, auto)
[PROOF STATE]
proof (state)
this:
prod (($$) Sum) ((\<lambda>x. (x, permutation_insert a a p x)) ` ({0..<n} - {a})) = prod (($$) Sum) {(i', permutation_insert a a p i') |i'. i' \<in> {0..<n} - {a}}

goal (1 subgoal):
 1. (\<Prod>i\<in>{0..<n} - {a}. Sum $$ (i, permutation_insert a a p i)) = (\<Prod>i = 0..<n - 1. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (i, p i))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
prod (($$) Sum) ((\<lambda>x. (x, permutation_insert a a p x)) ` ({0..<n} - {a})) = prod (($$) Sum) {(i', permutation_insert a a p i') |i'. i' \<in> {0..<n} - {a}}

goal (1 subgoal):
 1. (\<Prod>i\<in>{0..<n} - {a}. Sum $$ (i, permutation_insert a a p i)) = (\<Prod>i = 0..<n - 1. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (i, p i))
[PROOF STEP]
have "\<dots> = prod (($$) Sum) ((\<lambda> i. (?i i, ?i (p i))) ` {0 ..< ?n})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod (($$) Sum) {(i', permutation_insert a a p i') |i'. i' \<in> {0..<n} - {a}} = prod (($$) Sum) ((\<lambda>i. (insert_index a i, insert_index a (p i))) ` {0..<n - 1})
[PROOF STEP]
unfolding Determinant.foo[of a ?n a, unfolded n, OF a a p]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod (($$) Sum) {(insert_index a i'', insert_index a (p i'')) |i''. i'' < n - 1} = prod (($$) Sum) ((\<lambda>i. (insert_index a i, insert_index a (p i))) ` {0..<n - 1})
[PROOF STEP]
by (rule arg_cong[of _ _ "prod _"], auto)
[PROOF STATE]
proof (state)
this:
prod (($$) Sum) {(i', permutation_insert a a p i') |i'. i' \<in> {0..<n} - {a}} = prod (($$) Sum) ((\<lambda>i. (insert_index a i, insert_index a (p i))) ` {0..<n - 1})

goal (1 subgoal):
 1. (\<Prod>i\<in>{0..<n} - {a}. Sum $$ (i, permutation_insert a a p i)) = (\<Prod>i = 0..<n - 1. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (i, p i))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
prod (($$) Sum) {(i', permutation_insert a a p i') |i'. i' \<in> {0..<n} - {a}} = prod (($$) Sum) ((\<lambda>i. (insert_index a i, insert_index a (p i))) ` {0..<n - 1})

goal (1 subgoal):
 1. (\<Prod>i\<in>{0..<n} - {a}. Sum $$ (i, permutation_insert a a p i)) = (\<Prod>i = 0..<n - 1. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (i, p i))
[PROOF STEP]
have "\<dots> = prod (\<lambda> i. Sum $$ (?i i, ?i (p i))) {0 ..< ?n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod (($$) Sum) ((\<lambda>i. (insert_index a i, insert_index a (p i))) ` {0..<n - 1}) = (\<Prod>i = 0..<n - 1. Sum $$ (insert_index a i, insert_index a (p i)))
[PROOF STEP]
proof (subst prod.reindex, unfold o_def)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. inj_on (\<lambda>i. (insert_index a i, insert_index a (p i))) {0..<n - 1}
 2. (\<Prod>x = 0..<n - 1. Sum $$ (insert_index a x, insert_index a (p x))) = (\<Prod>i = 0..<n - 1. Sum $$ (insert_index a i, insert_index a (p i)))
[PROOF STEP]
show "inj_on (\<lambda>i. (?i i, ?i (p i))) {0..<?n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (\<lambda>i. (insert_index a i, insert_index a (p i))) {0..<n - 1}
[PROOF STEP]
using insert_index_inj_on[of a]
[PROOF STATE]
proof (prove)
using this:
inj_on (insert_index a) ?S

goal (1 subgoal):
 1. inj_on (\<lambda>i. (insert_index a i, insert_index a (p i))) {0..<n - 1}
[PROOF STEP]
by (auto simp: inj_on_def)
[PROOF STATE]
proof (state)
this:
inj_on (\<lambda>i. (insert_index a i, insert_index a (p i))) {0..<n - 1}

goal (1 subgoal):
 1. (\<Prod>x = 0..<n - 1. Sum $$ (insert_index a x, insert_index a (p x))) = (\<Prod>i = 0..<n - 1. Sum $$ (insert_index a i, insert_index a (p i)))
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
prod (($$) Sum) ((\<lambda>i. (insert_index a i, insert_index a (p i))) ` {0..<n - 1}) = (\<Prod>i = 0..<n - 1. Sum $$ (insert_index a i, insert_index a (p i)))

goal (1 subgoal):
 1. (\<Prod>i\<in>{0..<n} - {a}. Sum $$ (i, permutation_insert a a p i)) = (\<Prod>i = 0..<n - 1. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (i, p i))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
prod (($$) Sum) ((\<lambda>i. (insert_index a i, insert_index a (p i))) ` {0..<n - 1}) = (\<Prod>i = 0..<n - 1. Sum $$ (insert_index a i, insert_index a (p i)))

goal (1 subgoal):
 1. (\<Prod>i\<in>{0..<n} - {a}. Sum $$ (i, permutation_insert a a p i)) = (\<Prod>i = 0..<n - 1. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (i, p i))
[PROOF STEP]
have "\<dots> = (\<Prod>i = 0..<?n. ?B $$ (i, p i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>i = 0..<n - 1. Sum $$ (insert_index a i, insert_index a (p i))) = (\<Prod>i = 0..<n - 1. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (i, p i))
[PROOF STEP]
proof (rule prod.cong[OF refl], rename_tac i)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<in> {0..<n - 1} \<Longrightarrow> Sum $$ (insert_index a i, insert_index a (p i)) = ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (i, p i)
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<in> {0..<n - 1} \<Longrightarrow> Sum $$ (insert_index a i, insert_index a (p i)) = ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (i, p i)
[PROOF STEP]
assume "j \<in> {0 ..< ?n}"
[PROOF STATE]
proof (state)
this:
j \<in> {0..<n - 1}

goal (1 subgoal):
 1. \<And>i. i \<in> {0..<n - 1} \<Longrightarrow> Sum $$ (insert_index a i, insert_index a (p i)) = ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (i, p i)
[PROOF STEP]
hence j: "j < ?n"
[PROOF STATE]
proof (prove)
using this:
j \<in> {0..<n - 1}

goal (1 subgoal):
 1. j < n - 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j < n - 1

goal (1 subgoal):
 1. \<And>i. i \<in> {0..<n - 1} \<Longrightarrow> Sum $$ (insert_index a i, insert_index a (p i)) = ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (i, p i)
[PROOF STEP]
with p
[PROOF STATE]
proof (chain)
picking this:
p permutes {0..<n - 1}
j < n - 1
[PROOF STEP]
have pj: "p j < ?n"
[PROOF STATE]
proof (prove)
using this:
p permutes {0..<n - 1}
j < n - 1

goal (1 subgoal):
 1. p j < n - 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p j < n - 1

goal (1 subgoal):
 1. \<And>i. i \<in> {0..<n - 1} \<Longrightarrow> Sum $$ (insert_index a i, insert_index a (p i)) = ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (i, p i)
[PROOF STEP]
from j pj
[PROOF STATE]
proof (chain)
picking this:
j < n - 1
p j < n - 1
[PROOF STEP]
have jj: "?i j < n" "?i (p j) < n"
[PROOF STATE]
proof (prove)
using this:
j < n - 1
p j < n - 1

goal (1 subgoal):
 1. insert_index a j < n &&& insert_index a (p j) < n
[PROOF STEP]
by (auto simp: insert_index_def)
[PROOF STATE]
proof (state)
this:
insert_index a j < n
insert_index a (p j) < n

goal (1 subgoal):
 1. \<And>i. i \<in> {0..<n - 1} \<Longrightarrow> Sum $$ (insert_index a i, insert_index a (p i)) = ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (i, p i)
[PROOF STEP]
let ?jj = "(?i j, ?i (p j))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<in> {0..<n - 1} \<Longrightarrow> Sum $$ (insert_index a i, insert_index a (p i)) = ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (i, p i)
[PROOF STEP]
note index_adj = mat_delete_index[of _ ?n, unfolded n, OF _ a a j pj]
[PROOF STATE]
proof (state)
this:
?A \<in> carrier_mat n n \<Longrightarrow> ?A $$ (insert_index a j, insert_index a (p j)) = mat_delete ?A a a $$ (j, p j)

goal (1 subgoal):
 1. \<And>i. i \<in> {0..<n - 1} \<Longrightarrow> Sum $$ (insert_index a i, insert_index a (p i)) = ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (i, p i)
[PROOF STEP]
have "Sum $$ ?jj = lam $$ ?jj + mA $$ ?jj"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sum $$ (insert_index a j, insert_index a (p j)) = lam $$ (insert_index a j, insert_index a (p j)) + mA $$ (insert_index a j, insert_index a (p j))
[PROOF STEP]
unfolding Sum_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (lam + mA) $$ (insert_index a j, insert_index a (p j)) = lam $$ (insert_index a j, insert_index a (p j)) + mA $$ (insert_index a j, insert_index a (p j))
[PROOF STEP]
using jj A lam mA
[PROOF STATE]
proof (prove)
using this:
insert_index a j < n
insert_index a (p j) < n
A \<in> carrier_mat n n
lam \<in> carrier_mat n n
mA \<in> carrier_mat n n

goal (1 subgoal):
 1. (lam + mA) $$ (insert_index a j, insert_index a (p j)) = lam $$ (insert_index a j, insert_index a (p j)) + mA $$ (insert_index a j, insert_index a (p j))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Sum $$ (insert_index a j, insert_index a (p j)) = lam $$ (insert_index a j, insert_index a (p j)) + mA $$ (insert_index a j, insert_index a (p j))

goal (1 subgoal):
 1. \<And>i. i \<in> {0..<n - 1} \<Longrightarrow> Sum $$ (insert_index a i, insert_index a (p i)) = ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (i, p i)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Sum $$ (insert_index a j, insert_index a (p j)) = lam $$ (insert_index a j, insert_index a (p j)) + mA $$ (insert_index a j, insert_index a (p j))

goal (1 subgoal):
 1. \<And>i. i \<in> {0..<n - 1} \<Longrightarrow> Sum $$ (insert_index a i, insert_index a (p i)) = ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (i, p i)
[PROOF STEP]
have "\<dots> = ?B $$ (j, p j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lam $$ (insert_index a j, insert_index a (p j)) + mA $$ (insert_index a j, insert_index a (p j)) = ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (j, p j)
[PROOF STEP]
unfolding index_adj[OF mA] index_adj[OF lam]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_delete lam a a $$ (j, p j) + mat_delete mA a a $$ (j, p j) = ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (j, p j)
[PROOF STEP]
using j pj A
[PROOF STATE]
proof (prove)
using this:
j < n - 1
p j < n - 1
A \<in> carrier_mat n n

goal (1 subgoal):
 1. mat_delete lam a a $$ (j, p j) + mat_delete mA a a $$ (j, p j) = ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (j, p j)
[PROOF STEP]
by (simp add: mA_def lam_def mat_delete_def)
[PROOF STATE]
proof (state)
this:
lam $$ (insert_index a j, insert_index a (p j)) + mA $$ (insert_index a j, insert_index a (p j)) = ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (j, p j)

goal (1 subgoal):
 1. \<And>i. i \<in> {0..<n - 1} \<Longrightarrow> Sum $$ (insert_index a i, insert_index a (p i)) = ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (i, p i)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Sum $$ (insert_index a j, insert_index a (p j)) = ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (j, p j)
[PROOF STEP]
show "Sum $$ ?jj = ?B $$ (j, p j)"
[PROOF STATE]
proof (prove)
using this:
Sum $$ (insert_index a j, insert_index a (p j)) = ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (j, p j)

goal (1 subgoal):
 1. Sum $$ (insert_index a j, insert_index a (p j)) = ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (j, p j)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Sum $$ (insert_index a j, insert_index a (p j)) = ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (j, p j)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Prod>i = 0..<n - 1. Sum $$ (insert_index a i, insert_index a (p i))) = (\<Prod>i = 0..<n - 1. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (i, p i))

goal (1 subgoal):
 1. (\<Prod>i\<in>{0..<n} - {a}. Sum $$ (i, permutation_insert a a p i)) = (\<Prod>i = 0..<n - 1. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (i, p i))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Prod>i\<in>{0..<n} - {a}. Sum $$ (i, permutation_insert a a p i)) = (\<Prod>i = 0..<n - 1. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (i, p i))
[PROOF STEP]
show "(\<Prod>i\<in>{0..<n} - {a}. Sum $$ (i, ?p i)) = (\<Prod>i = 0..<?n. ?B $$ (i, p i))"
[PROOF STATE]
proof (prove)
using this:
(\<Prod>i\<in>{0..<n} - {a}. Sum $$ (i, permutation_insert a a p i)) = (\<Prod>i = 0..<n - 1. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (i, p i))

goal (1 subgoal):
 1. (\<Prod>i\<in>{0..<n} - {a}. Sum $$ (i, permutation_insert a a p i)) = (\<Prod>i = 0..<n - 1. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (i, p i))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<Prod>i\<in>{0..<n} - {a}. Sum $$ (i, permutation_insert a a p i)) = (\<Prod>i = 0..<n - 1. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (i, p i))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
g (permutation_insert a a p) a = of_int (sign p) * (\<Prod>i = 0..<n - 1. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) $$ (i, p i))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>p | p permutes {0..<n} \<and> p a = a. g p a) = det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a))

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>p | p permutes {0..<n} \<and> p a = a. g p a) = det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a))

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
have "\<dots> = char_poly (mat_delete A a a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) = char_poly (mat_delete A a a)
[PROOF STEP]
unfolding char_poly_def char_poly_matrix_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) = det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row (mat_delete A a a)) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a))
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n

goal (1 subgoal):
 1. det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) = det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row (mat_delete A a a)) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) = char_poly (mat_delete A a a)

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (n - 1) + map_mat (\<lambda>a. [:- a:]) (mat_delete A a a)) = char_poly (mat_delete A a a)

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
note calculation
[PROOF STATE]
proof (state)
this:
(\<Sum>p | p permutes {0..<n}. f p a) = char_poly (mat_delete A a a)

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?a4 < n \<Longrightarrow> (\<Sum>p | p permutes {0..<n}. f p ?a4) = char_poly (mat_delete A ?a4 ?a4)

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
note to_char_poly = this
[PROOF STATE]
proof (state)
this:
?a4 < n \<Longrightarrow> (\<Sum>p | p permutes {0..<n}. f p ?a4) = char_poly (mat_delete A ?a4 ?a4)

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
have "pderiv (char_poly A) = pderiv (?det Sum)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pderiv (char_poly A) = pderiv (det Sum)
[PROOF STEP]
unfolding char_poly_def char_poly_matrix_def id lam_def mA_def Sum_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pderiv (det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A)) = pderiv (det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pderiv (char_poly A) = pderiv (det Sum)

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
pderiv (char_poly A) = pderiv (det Sum)

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
have "\<dots> = sum (\<lambda> p. pderiv (signof p * ?e p)) ?P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pderiv (det Sum) = (\<Sum>p | p permutes {0..<n}. pderiv (of_int (sign p) * (\<Prod>i = 0..<n. Sum $$ (i, p i))))
[PROOF STEP]
unfolding det_def'[OF Sum]
    pderiv_sum
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>{p. p permutes {0..<n}}. pderiv (of_int (sign i) * (\<Prod>ia = 0..<n. Sum $$ (ia, i ia)))) = (\<Sum>p | p permutes {0..<n}. pderiv (of_int (sign p) * (\<Prod>i = 0..<n. Sum $$ (i, p i))))
[PROOF STEP]
by (rule sum.cong, auto)
[PROOF STATE]
proof (state)
this:
pderiv (det Sum) = (\<Sum>p | p permutes {0..<n}. pderiv (of_int (sign p) * (\<Prod>i = 0..<n. Sum $$ (i, p i))))

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
pderiv (det Sum) = (\<Sum>p | p permutes {0..<n}. pderiv (of_int (sign p) * (\<Prod>i = 0..<n. Sum $$ (i, p i))))

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
have "\<dots> = sum (\<lambda> p. (\<Sum>a = 0..<n. f p a)) ?P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>p | p permutes {0..<n}. pderiv (of_int (sign p) * (\<Prod>i = 0..<n. Sum $$ (i, p i)))) = (\<Sum>p | p permutes {0..<n}. sum (f p) {0..<n})
[PROOF STEP]
by (rule sum.cong[OF refl], subst to_f, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>p | p permutes {0..<n}. pderiv (of_int (sign p) * (\<Prod>i = 0..<n. Sum $$ (i, p i)))) = (\<Sum>p | p permutes {0..<n}. sum (f p) {0..<n})

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>p | p permutes {0..<n}. pderiv (of_int (sign p) * (\<Prod>i = 0..<n. Sum $$ (i, p i)))) = (\<Sum>p | p permutes {0..<n}. sum (f p) {0..<n})

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
have "\<dots> = (\<Sum>a = 0..<n. sum (\<lambda> p. f p a) ?P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>p | p permutes {0..<n}. sum (f p) {0..<n}) = (\<Sum>a = 0..<n. \<Sum>p | p permutes {0..<n}. f p a)
[PROOF STEP]
by (rule sum.swap)
[PROOF STATE]
proof (state)
this:
(\<Sum>p | p permutes {0..<n}. sum (f p) {0..<n}) = (\<Sum>a = 0..<n. \<Sum>p | p permutes {0..<n}. f p a)

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>p | p permutes {0..<n}. sum (f p) {0..<n}) = (\<Sum>a = 0..<n. \<Sum>p | p permutes {0..<n}. f p a)

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
have "\<dots> = (\<Sum>a <n. char_poly (mat_delete A a a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>a = 0..<n. \<Sum>p | p permutes {0..<n}. f p a) = (\<Sum>a<n. char_poly (mat_delete A a a))
[PROOF STEP]
by (rule sum.cong, auto simp: to_char_poly)
[PROOF STATE]
proof (state)
this:
(\<Sum>a = 0..<n. \<Sum>p | p permutes {0..<n}. f p a) = (\<Sum>a<n. char_poly (mat_delete A a a))

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
pderiv (char_poly A) = (\<Sum>a<n. char_poly (mat_delete A a a))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
pderiv (char_poly A) = (\<Sum>a<n. char_poly (mat_delete A a a))

goal (1 subgoal):
 1. pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_delete A i i))

goal:
No subgoals!
[PROOF STEP]
qed