mathlib3
1f6bbf9e - feat(analysis/special_functions/complex/arg): `arg_conj`, `arg_inv` lemmas (#11479)

Commit
3 years ago
feat(analysis/special_functions/complex/arg): `arg_conj`, `arg_inv` lemmas (#11479) Add lemmas giving the values of `arg (conj x)` and `arg x⁻¹`, both for `arg` as a real number and `arg` coerced to `real.angle` (the latter function being better behaved because it avoids case distinctions around getting a result into the interval (-π, π]).
Author
Parents
Loading