mathlib3

6e9b0112 - feat(linear_algebra/orientation): composing with linear equivs and determinant (#10737)

feat(linear_algebra/orientation): composing with linear equivs and determinant (#10737) Add lemmas that composing an alternating map with a linear equiv using `comp_linear_map`, or composing a basis with a linear equiv using `basis.map`, produces the same orientation if and only if the determinant of that linear equiv is positive. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>