equal
deleted
inserted
replaced
3 *) |
3 *) |
4 |
4 |
5 header {* Traces, Determinant of square matrices and some properties *} |
5 header {* Traces, Determinant of square matrices and some properties *} |
6 |
6 |
7 theory Determinants |
7 theory Determinants |
8 imports Euclidean_Space Permutations |
8 imports Euclidean_Space Permutations |
9 begin |
9 begin |
10 |
10 |
11 subsection{* First some facts about products*} |
11 subsection{* First some facts about products*} |
12 lemma setprod_insert_eq: "finite A \<Longrightarrow> setprod f (insert a A) = (if a \<in> A then setprod f A else f a * setprod f A)" |
12 lemma setprod_insert_eq: "finite A \<Longrightarrow> setprod f (insert a A) = (if a \<in> A then setprod f A else f a * setprod f A)" |
13 apply clarsimp |
13 apply clarsimp |