Summary
- Linear_Algebra: generalize linear_surjective_right/injective_left_inverse to real vector spaces
- Linear_Algebra: generalize linear_independent_extend to all real vector spaces
- Linear_Algebra: alternative representation of linear combination
- Linear_Algebra: move abstract concepts to front
The file was modified | src/HOL/Multivariate_Analysis/Linear_Algebra.thy (diff) |
The file was modified | src/HOL/Multivariate_Analysis/Linear_Algebra.thy (diff) |
The file was modified | src/HOL/Multivariate_Analysis/Linear_Algebra.thy (diff) |
The file was modified | src/HOL/Multivariate_Analysis/Linear_Algebra.thy (diff) |