Mathlib v3 is deprecated. Go to Mathlib v4

Theorem complex.arg_cos_add_sin_mul_I_eq_to_Ioc_mod

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) …
Added complex.arg_cos_add_sin_mul_I_eq_to_Ioc_modView on Github →