Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-14 23:58 5d7ab6e9

View on Github →

feat(analysis/inner_product_space/two_dim): volume/area form of negated orientation (#16939)

Estimated changes

Modified src/analysis/inner_product_space/orientation.lean

added theorem orientation.volume_form_neg_orientation

added theorem orientation.volume_form_robust_neg

modified theorem orientation.volume_form_zero_neg

added theorem orthonormal_basis.det_eq_neg_det_of_opposite_orientation

added theorem orthonormal_basis.det_to_matrix_orthonormal_basis_of_opposite_orientation

Modified src/analysis/inner_product_space/two_dim.lean

added theorem orientation.area_form_neg_orientation

added theorem orientation.kahler_neg_orientation

added theorem orientation.right_angle_rotation_neg_orientation

added theorem orientation.right_angle_rotation_trans_neg_orientation