Mathlib v3 is deprecated. Go to Mathlib v4

Theorem complex.arg_cos_add_sin_mul_I_eq_mul_fract

Modification history

2022-08-10 15:00
src/analysis/special_functions/complex/arg.lean
feat(algebra/order/to_interval_mod): reducing to an interval modulo its length (#15966) …
Deleted complex.arg_cos_add_sin_mul_I_eq_mul_fractView on Github →
2022-02-10 20:43
src/analysis/special_functions/complex/arg.lean
feat(analysis/special_functions/complex/arg): `arg_mul`, `arg_div` lemmas (#11903) …
Added complex.arg_cos_add_sin_mul_I_eq_mul_fractView on Github →