Commit 2023-05-26 12:18 12200504

View on Github →

feat: port Geometry.Euclidean.Angle.Unoriented.Basic (#4376)

Estimated changes

Modified Mathlib.lean

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

added def InnerProductGeometry.angle

added theorem InnerProductGeometry.angle_add_angle_eq_pi_of_angle_eq_pi

added theorem InnerProductGeometry.angle_comm

added theorem InnerProductGeometry.angle_eq_pi_iff

added theorem InnerProductGeometry.angle_eq_zero_iff

added theorem InnerProductGeometry.angle_le_pi

added theorem InnerProductGeometry.angle_neg_left

added theorem InnerProductGeometry.angle_neg_neg

added theorem InnerProductGeometry.angle_neg_right

added theorem InnerProductGeometry.angle_neg_self_of_nonzero

added theorem InnerProductGeometry.angle_nonneg

added theorem InnerProductGeometry.angle_self

added theorem InnerProductGeometry.angle_self_neg_of_nonzero

added theorem InnerProductGeometry.angle_smul_left_of_neg

added theorem InnerProductGeometry.angle_smul_left_of_pos

added theorem InnerProductGeometry.angle_smul_right_of_neg

added theorem InnerProductGeometry.angle_smul_right_of_pos

added theorem InnerProductGeometry.angle_smul_smul

added theorem InnerProductGeometry.angle_zero_left

added theorem InnerProductGeometry.angle_zero_right

added theorem InnerProductGeometry.continuousAt_angle

added theorem InnerProductGeometry.cos_angle

added theorem InnerProductGeometry.cos_angle_mul_norm_mul_norm

added theorem InnerProductGeometry.cos_eq_neg_one_iff_angle_eq_pi

added theorem InnerProductGeometry.cos_eq_one_iff_angle_eq_zero

added theorem InnerProductGeometry.cos_eq_zero_iff_angle_eq_pi_div_two

added theorem InnerProductGeometry.inner_eq_mul_norm_iff_angle_eq_zero

added theorem InnerProductGeometry.inner_eq_mul_norm_of_angle_eq_zero

added theorem InnerProductGeometry.inner_eq_neg_mul_norm_iff_angle_eq_pi

added theorem InnerProductGeometry.inner_eq_neg_mul_norm_of_angle_eq_pi

added theorem InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two

added theorem InnerProductGeometry.norm_add_eq_add_norm_iff_angle_eq_zero

added theorem InnerProductGeometry.norm_add_eq_add_norm_of_angle_eq_zero

added theorem InnerProductGeometry.norm_add_eq_norm_sub_iff_angle_eq_pi_div_two

added theorem InnerProductGeometry.norm_sub_eq_abs_sub_norm_iff_angle_eq_zero

added theorem InnerProductGeometry.norm_sub_eq_abs_sub_norm_of_angle_eq_zero

added theorem InnerProductGeometry.norm_sub_eq_add_norm_iff_angle_eq_pi

added theorem InnerProductGeometry.norm_sub_eq_add_norm_of_angle_eq_pi

added theorem InnerProductGeometry.sin_angle_mul_norm_mul_norm

added theorem InnerProductGeometry.sin_eq_one_iff_angle_eq_pi_div_two

added theorem InnerProductGeometry.sin_eq_zero_iff_angle_eq_zero_or_angle_eq_pi

added theorem LinearIsometry.angle_map

added theorem Submodule.angle_coe