Commit 2023-06-13 08:12 6845e263

View on Github →

feat: port Geometry.Euclidean.Angle.Oriented.Basic (#4966)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean

added theorem Orientation.abs_oangle_sub_left_toReal_lt_pi_div_two

added theorem Orientation.abs_oangle_sub_right_toReal_lt_pi_div_two

added theorem Orientation.angle_eq_abs_oangle_toReal

added theorem Orientation.angle_eq_iff_oangle_eq_of_sign_eq

added theorem Orientation.continuousAt_oangle

added theorem Orientation.cos_oangle_eq_cos_angle

added theorem Orientation.cos_oangle_eq_inner_div_norm_mul_norm

added theorem Orientation.eq_iff_norm_eq_and_oangle_eq_zero

added theorem Orientation.eq_iff_norm_eq_of_oangle_eq_zero

added theorem Orientation.eq_iff_oangle_eq_zero_of_norm_eq

added theorem Orientation.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero

added theorem Orientation.eq_zero_or_oangle_eq_iff_inner_eq_zero

added theorem Orientation.inner_eq_norm_mul_norm_mul_cos_oangle

added theorem Orientation.inner_eq_zero_of_oangle_eq_neg_pi_div_two

added theorem Orientation.inner_eq_zero_of_oangle_eq_pi_div_two

added theorem Orientation.inner_rev_eq_zero_of_oangle_eq_neg_pi_div_two

added theorem Orientation.inner_rev_eq_zero_of_oangle_eq_pi_div_two

added theorem Orientation.left_ne_zero_of_oangle_eq_neg_pi_div_two

added theorem Orientation.left_ne_zero_of_oangle_eq_pi

added theorem Orientation.left_ne_zero_of_oangle_eq_pi_div_two

added theorem Orientation.left_ne_zero_of_oangle_ne_zero

added theorem Orientation.left_ne_zero_of_oangle_sign_eq_neg_one

added theorem Orientation.left_ne_zero_of_oangle_sign_eq_one

added theorem Orientation.left_ne_zero_of_oangle_sign_ne_zero

added theorem Orientation.ne_of_oangle_eq_neg_pi_div_two

added theorem Orientation.ne_of_oangle_eq_pi

added theorem Orientation.ne_of_oangle_eq_pi_div_two

added theorem Orientation.ne_of_oangle_ne_zero

added theorem Orientation.ne_of_oangle_sign_eq_neg_one

added theorem Orientation.ne_of_oangle_sign_eq_one

added theorem Orientation.ne_of_oangle_sign_ne_zero

added def Orientation.oangle

added theorem Orientation.oangle_add

added theorem Orientation.oangle_add_cyc3

added theorem Orientation.oangle_add_cyc3_neg_left

added theorem Orientation.oangle_add_cyc3_neg_right

added theorem Orientation.oangle_add_oangle_rev

added theorem Orientation.oangle_add_oangle_rev_neg_left

added theorem Orientation.oangle_add_oangle_rev_neg_right

added theorem Orientation.oangle_add_swap

added theorem Orientation.oangle_eq_angle_of_sign_eq_one

added theorem Orientation.oangle_eq_angle_or_eq_neg_angle

added theorem Orientation.oangle_eq_neg_angle_of_sign_eq_neg_one

added theorem Orientation.oangle_eq_of_angle_eq_of_sign_eq

added theorem Orientation.oangle_eq_pi_iff_angle_eq_pi

added theorem Orientation.oangle_eq_pi_iff_oangle_rev_eq_pi

added theorem Orientation.oangle_eq_pi_iff_sameRay_neg

added theorem Orientation.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq

added theorem Orientation.oangle_eq_zero_iff_angle_eq_zero

added theorem Orientation.oangle_eq_zero_iff_oangle_rev_eq_zero

added theorem Orientation.oangle_eq_zero_iff_sameRay

added theorem Orientation.oangle_eq_zero_or_eq_pi_iff_not_linearIndependent

added theorem Orientation.oangle_eq_zero_or_eq_pi_iff_right_eq_smul

added theorem Orientation.oangle_map

added theorem Orientation.oangle_map_complex

added theorem Orientation.oangle_ne_zero_and_ne_pi_iff_linearIndependent

added theorem Orientation.oangle_neg_left

added theorem Orientation.oangle_neg_left_eq_neg_right

added theorem Orientation.oangle_neg_neg

added theorem Orientation.oangle_neg_orientation_eq_neg

added theorem Orientation.oangle_neg_right

added theorem Orientation.oangle_neg_self_left

added theorem Orientation.oangle_neg_self_right

added theorem Orientation.oangle_rev

added theorem Orientation.oangle_self

added theorem Orientation.oangle_sign_add_left

added theorem Orientation.oangle_sign_add_right

added theorem Orientation.oangle_sign_add_smul_left

added theorem Orientation.oangle_sign_neg_left

added theorem Orientation.oangle_sign_neg_right

added theorem Orientation.oangle_sign_smul_add_right

added theorem Orientation.oangle_sign_smul_add_smul_left

added theorem Orientation.oangle_sign_smul_add_smul_right

added theorem Orientation.oangle_sign_smul_add_smul_smul_add_smul

added theorem Orientation.oangle_sign_smul_left

added theorem Orientation.oangle_sign_smul_right

added theorem Orientation.oangle_sign_smul_sub_left

added theorem Orientation.oangle_sign_smul_sub_right

added theorem Orientation.oangle_sign_sub_left

added theorem Orientation.oangle_sign_sub_left_eq_neg

added theorem Orientation.oangle_sign_sub_left_swap

added theorem Orientation.oangle_sign_sub_right

added theorem Orientation.oangle_sign_sub_right_eq_neg

added theorem Orientation.oangle_sign_sub_right_swap

added theorem Orientation.oangle_sign_sub_smul_left

added theorem Orientation.oangle_sign_sub_smul_right

added theorem Orientation.oangle_smul_add_right_eq_zero_or_eq_pi_iff

added theorem Orientation.oangle_smul_left_of_neg

added theorem Orientation.oangle_smul_left_of_pos

added theorem Orientation.oangle_smul_left_self_of_nonneg

added theorem Orientation.oangle_smul_right_of_neg

added theorem Orientation.oangle_smul_right_of_pos

added theorem Orientation.oangle_smul_right_self_of_nonneg

added theorem Orientation.oangle_smul_smul_self_of_nonneg

added theorem Orientation.oangle_sub_eq_oangle_sub_rev_of_norm_eq

added theorem Orientation.oangle_sub_left

added theorem Orientation.oangle_sub_right

added theorem Orientation.oangle_zero_left

added theorem Orientation.oangle_zero_right

added theorem Orientation.right_ne_zero_of_oangle_eq_neg_pi_div_two

added theorem Orientation.right_ne_zero_of_oangle_eq_pi

added theorem Orientation.right_ne_zero_of_oangle_eq_pi_div_two

added theorem Orientation.right_ne_zero_of_oangle_ne_zero

added theorem Orientation.right_ne_zero_of_oangle_sign_eq_neg_one

added theorem Orientation.right_ne_zero_of_oangle_sign_eq_one

added theorem Orientation.right_ne_zero_of_oangle_sign_ne_zero

added theorem Orientation.two_zsmul_oangle_left_of_span_eq

added theorem Orientation.two_zsmul_oangle_neg_left

added theorem Orientation.two_zsmul_oangle_neg_right

added theorem Orientation.two_zsmul_oangle_neg_self_left

added theorem Orientation.two_zsmul_oangle_neg_self_right

added theorem Orientation.two_zsmul_oangle_of_span_eq_of_span_eq

added theorem Orientation.two_zsmul_oangle_right_of_span_eq

added theorem Orientation.two_zsmul_oangle_smul_left_of_ne_zero

added theorem Orientation.two_zsmul_oangle_smul_left_self

added theorem Orientation.two_zsmul_oangle_smul_right_of_ne_zero

added theorem Orientation.two_zsmul_oangle_smul_right_self

added theorem Orientation.two_zsmul_oangle_smul_smul_self