Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-30 23:37 a753abcf

View on Github →

feat(linear_algebra/{basis, determinant, orientation}): determinant of adjust_to_orientation of a basis (#16476) Performing the operation adjust_to_orientation on a basis either preserves the determinant with respect to that basis, or negates it. Formalized as part of the Sphere Eversion project.

Estimated changes