mathlib

a753abcf - feat(linear_algebra/{basis, determinant, orientation}): determinant of `adjust_to_orientation` of a basis (#16476)

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.