Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. Linear_Algebra: generalize linear_surjective_right/injective_left_inverse to real vector spaces
  2. Linear_Algebra: generalize linear_independent_extend to all real vector spaces
  3. Linear_Algebra: alternative representation of linear combination
  4. Linear_Algebra: move abstract concepts to front
Changeset 63053:4a108f280dc2 by hoelzl:
Linear_Algebra: generalize linear_surjective_right/injective_left_inverse to real vector spaces
The file was modified src/HOL/Multivariate_Analysis/Linear_Algebra.thy (diff)
Changeset 63052:c968bce3921e by hoelzl:
Linear_Algebra: generalize linear_independent_extend to all real vector spaces
The file was modified src/HOL/Multivariate_Analysis/Linear_Algebra.thy (diff)
Changeset 63051:e5e69206d52d by hoelzl:
Linear_Algebra: alternative representation of linear combination
The file was modified src/HOL/Multivariate_Analysis/Linear_Algebra.thy (diff)
Changeset 63050:ca4cce24c75d by hoelzl:
Linear_Algebra: move abstract concepts to front
The file was modified src/HOL/Multivariate_Analysis/Linear_Algebra.thy (diff)