Theorem Complex.arg_mul_real

Modification history

2023-11-16 23:07
Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
feat: add lemmas on Complex.arg (x * y) and Complex.log (x * y) (#8346) …
Added Complex.arg_mul_realView on Github →