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

Modified src/linear_algebra/orientation.lean

added def basis.adjust_to_orientation

added theorem basis.adjust_to_orientation_apply_eq_or_eq_neg

added theorem basis.orientation_adjust_to_orientation

added theorem basis.orientation_neg_single

added theorem basis.orientation_units_smul

added def orientation.some_basis

added theorem orientation.some_basis_orientation