Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-05 14:15 98b64f49

View on Github →

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.

Estimated changes