Commit 2023-05-17 05:45 44a2ae61

View on Github →

feat: port Analysis.Complex.Circle (#4014)

Estimated changes

added theorem abs_coe_circle
added def circle.toUnits
added theorem circle.toUnits_apply
added def circle
added theorem circle_def
added theorem coe_div_circle
added theorem coe_inv_circle
added theorem coe_inv_circle_eq_conj
added def expMapCircle
added def expMapCircleHom
added theorem expMapCircle_add
added theorem expMapCircle_apply
added theorem expMapCircle_neg
added theorem expMapCircle_sub
added theorem expMapCircle_zero
added theorem mem_circle_iff_abs
added theorem mem_circle_iff_normSq
added theorem ne_zero_of_mem_circle