Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-14 10:58 44351a9f

View on Github →

chore(analysis/complex/circle): add to_units and golf (#11435)

Estimated changes

added def circle.to_units
deleted def rotation_aux