Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-26 05:05 4f02336c

View on Github →

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.

Estimated changes

added theorem abs_coe_circle
deleted theorem abs_eq_of_mem_circle
modified theorem circle_def
modified theorem mem_circle_iff_abs
added theorem mem_circle_iff_norm_sq