equal
deleted
inserted
replaced
4 |
4 |
5 section \<open>Traces and Determinants of Square Matrices\<close> |
5 section \<open>Traces and Determinants of Square Matrices\<close> |
6 |
6 |
7 theory Determinants |
7 theory Determinants |
8 imports |
8 imports |
|
9 "HOL-Combinatorics.Permutations" |
9 Cartesian_Space |
10 Cartesian_Space |
10 "HOL-Library.Permutations" |
|
11 begin |
11 begin |
12 |
12 |
13 subsection \<open>Trace\<close> |
13 subsection \<open>Trace\<close> |
14 |
14 |
15 definition\<^marker>\<open>tag important\<close> trace :: "'a::semiring_1^'n^'n \<Rightarrow> 'a" |
15 definition\<^marker>\<open>tag important\<close> trace :: "'a::semiring_1^'n^'n \<Rightarrow> 'a" |