mathlib3

98b64f49 - feat(linear_algebra/orientation): bases from orientations (#11234)

feat(linear_algebra/orientation): bases from orientations (#11234) Add a lemma giving the orientation of a basis constructed with `units_smul`, and thus definitions and lemmas to construct a basis from an orientation.