Commit 2023-06-02 11:07 71abac05

View on Github →

feat: port Analysis.InnerProductSpace.Orientation (#4503)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean

modified theorem gramSchmidtOrthonormalBasis_det

Created Mathlib/Analysis/InnerProductSpace/Orientation.lean

added theorem Orientation.abs_volumeForm_apply_le

added theorem Orientation.abs_volumeForm_apply_of_orthonormal

added theorem Orientation.abs_volumeForm_apply_of_pairwise_orthogonal

added theorem Orientation.finOrthonormalBasis_orientation

added theorem Orientation.volumeForm_apply_le

added theorem Orientation.volumeForm_comp_linearIsometryEquiv

added theorem Orientation.volumeForm_map

added theorem Orientation.volumeForm_neg_orientation

added theorem Orientation.volumeForm_robust'

added theorem Orientation.volumeForm_robust

added theorem Orientation.volumeForm_robust_neg

added theorem Orientation.volumeForm_zero_neg

added theorem Orientation.volumeForm_zero_pos

added theorem OrthonormalBasis.abs_det_adjustToOrientation

added def OrthonormalBasis.adjustToOrientation

added theorem OrthonormalBasis.adjustToOrientation_apply_eq_or_eq_neg

added theorem OrthonormalBasis.det_adjustToOrientation

added theorem OrthonormalBasis.det_eq_neg_det_of_opposite_orientation

added theorem OrthonormalBasis.det_to_matrix_orthonormalBasis_of_opposite_orientation

added theorem OrthonormalBasis.det_to_matrix_orthonormalBasis_of_same_orientation

added theorem OrthonormalBasis.orientation_adjustToOrientation

added theorem OrthonormalBasis.orthonormal_adjustToOrientation

added theorem OrthonormalBasis.same_orientation_iff_det_eq_det

added theorem OrthonormalBasis.toBasis_adjustToOrientation