equal
deleted
inserted
replaced
5 section \<open>Traces, Determinant of square matrices and some properties\<close> |
5 section \<open>Traces, Determinant of square matrices and some properties\<close> |
6 |
6 |
7 theory Determinants |
7 theory Determinants |
8 imports |
8 imports |
9 Cartesian_Euclidean_Space |
9 Cartesian_Euclidean_Space |
10 "~~/src/HOL/Library/Permutations" |
10 "HOL-Library.Permutations" |
11 begin |
11 begin |
12 |
12 |
13 subsection \<open>Trace\<close> |
13 subsection \<open>Trace\<close> |
14 |
14 |
15 definition trace :: "'a::semiring_1^'n^'n \<Rightarrow> 'a" |
15 definition trace :: "'a::semiring_1^'n^'n \<Rightarrow> 'a" |