mathlib3
92ac8ff8 - feat(analysis/special_functions/complex/arg): `arg_coe_angle_eq_iff` (#12017)

Commit
4 years ago
feat(analysis/special_functions/complex/arg): `arg_coe_angle_eq_iff` (#12017) Add a lemma that `arg` of two numbers coerced to `real.angle` is equal if and only if `arg` is equal.
Author
Parents
Loading