arg): `continuous_at_arg_coe_angle` (#14980)

Commit

3 years ago

feat(analysis/special_functions/complex/arg): `continuous_at_arg_coe_angle` (#14980) Add the lemma that `complex.arg`, coerced to `real.angle`, is continuous except at 0.

Author

jsm28

Parents

8f391f56

mathlib 06ac34b8 - feat(analysis/special_functions/complex/arg): `continuous_at_arg_coe_angle` (#14980)

mathlib
06ac34b8 - feat(analysis/special_functions/complex/arg): `continuous_at_arg_coe_angle` (#14980)