Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-10 01:48 8b8f46e4

View on Github →

feat(analysis/complex/arg): link same_ray and complex.arg (#12764)

Estimated changes

Created src/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.same_ray_iff

added theorem complex.same_ray_of_arg_eq

Modified src/linear_algebra/ray.lean

modified theorem same_ray.zero_left

modified theorem same_ray.zero_right