changeset 41959 | b460124855b8 |
parent 38642 | 8fa437809c67 |
child 44133 | 691c52e900ca |
41958:5abc60a017e0 | 41959:b460124855b8 |
---|---|
1 (* Title: Library/Operator_Norm.thy |
1 (* Title: HOL/Multivariate_Analysis/Operator_Norm.thy |
2 Author: Amine Chaieb, University of Cambridge |
2 Author: Amine Chaieb, University of Cambridge |
3 *) |
3 *) |
4 |
4 |
5 header {* Operator Norm *} |
5 header {* Operator Norm *} |
6 |
6 |