Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-05-25 23:22
a6885a1a
View on Github →
feat: port Analysis.Complex.Arg (
#4355
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/Analysis/Complex/Arg.lean
added
theorem
Complex.abs_add_eq
added
theorem
Complex.abs_add_eq_iff
added
theorem
Complex.abs_sub_eq
added
theorem
Complex.abs_sub_eq_iff
added
theorem
Complex.sameRay_iff
added
theorem
Complex.sameRay_iff_arg_div_eq_zero
added
theorem
Complex.sameRay_of_arg_eq
Modified
Mathlib/Analysis/Convex/StrictConvexSpace.lean
Modified
Mathlib/Analysis/NormedSpace/Ray.lean