src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy
author hoelzl
Fri Dec 14 15:46:01 2012 +0100 (2012-12-14)
changeset 50526 899c9c4e4a4c
parent 44229 7e3a026f014f
child 56189 c4daa97ac57a
permissions -rw-r--r--
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
     1 theory Multivariate_Analysis
     2 imports Fashoda Extended_Real_Limits Determinants
     3 begin
     4 
     5 end