mathlib
47264da1 - feat(linear_algebra): tiny missing pieces (#4089)

Commit

5 years ago

feat(linear_algebra): tiny missing pieces (#4089) From the sphere eversion project.

References

Author

PatrickMassot

Parents