mathlib
93047c52 - feat(linear_algebra/determinant): linear coordinates are ratio of determinants (#10261)

Commit

4 years ago

feat(linear_algebra/determinant): linear coordinates are ratio of determinants (#10261) Formalized as part of the Sphere Eversion project.

Author

ocfnash

Parents