Commit 2024-03-01 17:22 5156e249

View on Github →

feat: Angle between complex numbers (#10226) Prove that the angle between two complex numbers is the absolute value of the argument of their quotient. From LeanAPAP

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Complex/Angle.lean

added theorem Complex.angle_div_left_eq_angle_mul_right

added theorem Complex.angle_div_right_eq_angle_mul_left

added theorem Complex.angle_eq_abs_arg

added theorem Complex.angle_exp_exp

added theorem Complex.angle_exp_one

added theorem Complex.angle_mul_left

added theorem Complex.angle_mul_right

added theorem Complex.angle_one_left

added theorem Complex.angle_one_right

Modified Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean

added theorem Complex.abs_arg_inv

added theorem Complex.abs_eq_one_iff'

added theorem Complex.arg_exp_mul_I

added theorem Complex.image_exp_Ioc_eq_sphere

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean

added theorem Real.arccos_eq_of_eq_cos

Modified Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean

deleted theorem EuclideanGeometry.angle_eq_left

deleted theorem EuclideanGeometry.angle_eq_of_ne

deleted theorem EuclideanGeometry.angle_eq_right

added theorem EuclideanGeometry.angle_self_left

added theorem EuclideanGeometry.angle_self_of_ne

added theorem EuclideanGeometry.angle_self_right

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