Commit 2023-05-08 05:55 39a42429

View on Github →

feat port: LinearAlgebra.Orientation (#3777) I had to add a bunch of set_option synthInstance.etaExperiment true, set_option maxHeartbeats and set_option synthInstance.maxHeartbeats to this file I tried to use the methods described in this Zulip thread to remove some of the maxHeartbeats but I was not successful.

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Orientation.lean

added theorem Basis.abs_det_adjustToOrientation

added def Basis.adjustToOrientation

added theorem Basis.adjustToOrientation_apply_eq_or_eq_neg

added theorem Basis.det_adjustToOrientation

added theorem Basis.map_orientation_eq_det_inv_smul

added theorem Basis.orientation_adjustToOrientation

added theorem Basis.orientation_comp_linearEquiv_eq_iff_det_pos

added theorem Basis.orientation_comp_linearEquiv_eq_neg_iff_det_neg

added theorem Basis.orientation_eq_iff_det_pos

added theorem Basis.orientation_eq_or_eq_neg

added theorem Basis.orientation_isEmpty

added theorem Basis.orientation_map

added theorem Basis.orientation_ne_iff_eq_neg

added theorem Basis.orientation_neg_single

added theorem Basis.orientation_unitsSMul

added theorem Orientation.eq_or_eq_neg

added theorem Orientation.eq_or_eq_neg_of_isEmpty

added def Orientation.map

added theorem Orientation.map_apply

added theorem Orientation.map_eq_det_inv_smul

added theorem Orientation.map_eq_iff_det_pos

added theorem Orientation.map_eq_neg_iff_det_neg

added theorem Orientation.map_of_isEmpty

added theorem Orientation.map_positiveOrientation_of_isEmpty

added theorem Orientation.map_refl

added theorem Orientation.map_symm

added theorem Orientation.ne_iff_eq_neg

added def Orientation.someBasis

added theorem Orientation.someBasis_orientation