Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-18 17:47 fb319896

View on Github →

refactor(geometry/euclidean/angle/oriented/basic): split out rotations (#18212) geometry.euclidean.angle.oriented.basic is 1489 lines long. Reduce it to 1032 lines by splitting out the definition of and results about rotation to a separate file. (No results in this file involve rotation in their proofs unless it's also involved in the statement.) There are no changes to API or proofs.

Estimated changes

Modified src/geometry/euclidean/angle/oriented/affine.lean

Modified src/geometry/euclidean/angle/oriented/basic.lean

deleted theorem orientation.det_rotation

deleted theorem orientation.eq_rotation_self_iff

deleted theorem orientation.eq_rotation_self_iff_angle_eq_zero

deleted theorem orientation.exists_linear_isometry_equiv_eq_of_det_pos

deleted theorem orientation.inner_eq_zero_iff_eq_zero_or_eq_smul_rotation_pi_div_two

deleted theorem orientation.inner_rotation_pi_div_two_left

deleted theorem orientation.inner_rotation_pi_div_two_left_smul

deleted theorem orientation.inner_rotation_pi_div_two_right

deleted theorem orientation.inner_rotation_pi_div_two_right_smul

deleted theorem orientation.inner_smul_rotation_pi_div_two_left

deleted theorem orientation.inner_smul_rotation_pi_div_two_right

deleted theorem orientation.inner_smul_rotation_pi_div_two_smul_left

deleted theorem orientation.inner_smul_rotation_pi_div_two_smul_right

deleted theorem orientation.kahler_rotation_left'

deleted theorem orientation.kahler_rotation_left

deleted theorem orientation.kahler_rotation_right

deleted theorem orientation.linear_equiv_det_rotation

deleted theorem orientation.neg_rotation

deleted theorem orientation.neg_rotation_neg_pi_div_two

deleted theorem orientation.neg_rotation_pi_div_two

deleted theorem orientation.oangle_eq_iff_eq_norm_div_norm_smul_rotation_of_ne_zero

deleted theorem orientation.oangle_eq_iff_eq_norm_div_norm_smul_rotation_or_eq_zero

deleted theorem orientation.oangle_eq_iff_eq_pos_smul_rotation_of_ne_zero

deleted theorem orientation.oangle_eq_iff_eq_pos_smul_rotation_or_eq_zero

deleted theorem orientation.oangle_rotation

deleted theorem orientation.oangle_rotation_left

deleted theorem orientation.oangle_rotation_oangle_left

deleted theorem orientation.oangle_rotation_oangle_right

deleted theorem orientation.oangle_rotation_right

deleted theorem orientation.oangle_rotation_self_left

deleted theorem orientation.oangle_rotation_self_right

deleted def orientation.rotation

deleted theorem orientation.rotation_apply

deleted def orientation.rotation_aux

deleted theorem orientation.rotation_aux_apply

deleted theorem orientation.rotation_eq_matrix_to_lin

deleted theorem orientation.rotation_eq_self_iff

deleted theorem orientation.rotation_eq_self_iff_angle_eq_zero

deleted theorem orientation.rotation_map

deleted theorem orientation.rotation_map_complex

deleted theorem orientation.rotation_neg_orientation_eq_neg

deleted theorem orientation.rotation_oangle_eq_iff_norm_eq

deleted theorem orientation.rotation_pi

deleted theorem orientation.rotation_pi_apply

deleted theorem orientation.rotation_pi_div_two

deleted theorem orientation.rotation_rotation

deleted theorem orientation.rotation_symm

deleted theorem orientation.rotation_symm_apply

deleted theorem orientation.rotation_trans

deleted theorem orientation.rotation_zero

Created src/geometry/euclidean/angle/oriented/rotation.lean

added theorem orientation.det_rotation

added theorem orientation.eq_rotation_self_iff

added theorem orientation.eq_rotation_self_iff_angle_eq_zero

added theorem orientation.exists_linear_isometry_equiv_eq_of_det_pos

added theorem orientation.inner_eq_zero_iff_eq_zero_or_eq_smul_rotation_pi_div_two

added theorem orientation.inner_rotation_pi_div_two_left

added theorem orientation.inner_rotation_pi_div_two_left_smul

added theorem orientation.inner_rotation_pi_div_two_right

added theorem orientation.inner_rotation_pi_div_two_right_smul

added theorem orientation.inner_smul_rotation_pi_div_two_left

added theorem orientation.inner_smul_rotation_pi_div_two_right

added theorem orientation.inner_smul_rotation_pi_div_two_smul_left

added theorem orientation.inner_smul_rotation_pi_div_two_smul_right

added theorem orientation.kahler_rotation_left'

added theorem orientation.kahler_rotation_left

added theorem orientation.kahler_rotation_right

added theorem orientation.linear_equiv_det_rotation

added theorem orientation.neg_rotation

added theorem orientation.neg_rotation_neg_pi_div_two

added theorem orientation.neg_rotation_pi_div_two

added theorem orientation.oangle_eq_iff_eq_norm_div_norm_smul_rotation_of_ne_zero

added theorem orientation.oangle_eq_iff_eq_norm_div_norm_smul_rotation_or_eq_zero

added theorem orientation.oangle_eq_iff_eq_pos_smul_rotation_of_ne_zero

added theorem orientation.oangle_eq_iff_eq_pos_smul_rotation_or_eq_zero

added theorem orientation.oangle_rotation

added theorem orientation.oangle_rotation_left

added theorem orientation.oangle_rotation_oangle_left

added theorem orientation.oangle_rotation_oangle_right

added theorem orientation.oangle_rotation_right

added theorem orientation.oangle_rotation_self_left

added theorem orientation.oangle_rotation_self_right

added def orientation.rotation

added theorem orientation.rotation_apply

added def orientation.rotation_aux

added theorem orientation.rotation_aux_apply

added theorem orientation.rotation_eq_matrix_to_lin

added theorem orientation.rotation_eq_self_iff

added theorem orientation.rotation_eq_self_iff_angle_eq_zero

added theorem orientation.rotation_map

added theorem orientation.rotation_map_complex

added theorem orientation.rotation_neg_orientation_eq_neg

added theorem orientation.rotation_oangle_eq_iff_norm_eq

added theorem orientation.rotation_pi

added theorem orientation.rotation_pi_apply

added theorem orientation.rotation_pi_div_two

added theorem orientation.rotation_rotation

added theorem orientation.rotation_symm

added theorem orientation.rotation_symm_apply

added theorem orientation.rotation_trans

added theorem orientation.rotation_zero