mathlib

4f02336c - chore(analysis/complex/circle): minor review (#11059)

chore(analysis/complex/circle): minor review (#11059) * use implicit arg in `mem_circle_iff_abs`; * rename `abs_eq_of_mem_circle` to `abs_coe_circle` to reflect the type of LHS; * add `mem_circle_iff_norm_sq`.