Commit 2021-12-23 16:32 6e9b0112

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.