equal
deleted
inserted
replaced
1 (* Title: HOL/Analysis/Determinants.thy |
1 (* Title: HOL/Analysis/Determinants.thy |
2 Author: Amine Chaieb, University of Cambridge; proofs reworked by LCP |
2 Author: Amine Chaieb, University of Cambridge; proofs reworked by LCP |
3 *) |
3 *) |
4 |
4 |
5 section \<open>Traces, Determinant of square matrices and some properties\<close> |
5 section \<open>Traces and Determinants of Square Matrices\<close> |
6 |
6 |
7 theory Determinants |
7 theory Determinants |
8 imports |
8 imports |
9 Cartesian_Space |
9 Cartesian_Space |
10 "HOL-Library.Permutations" |
10 "HOL-Library.Permutations" |