changeset 41959 | b460124855b8 |
parent 41891 | d37babdf5cae |
child 44142 | 8e27e0177518 |
41958:5abc60a017e0 | 41959:b460124855b8 |
---|---|
1 (* Title: Multivariate_Analysis/L2_Norm.thy |
1 (* Title: HOL/Multivariate_Analysis/L2_Norm.thy |
2 Author: Brian Huffman, Portland State University |
2 Author: Brian Huffman, Portland State University |
3 *) |
3 *) |
4 |
4 |
5 header {* Square root of sum of squares *} |
5 header {* Square root of sum of squares *} |
6 |
6 |