Mathlib v3 is deprecated. Go to Mathlib v4

Def real.angle

Modification history

2022-10-03 06:36
src/analysis/special_functions/trigonometric/angle.lean
feat(analysis/normed/group/add_circle): define the additive circle (#16201)
Modified real.angleView on Github →
2021-10-31 11:57
src/analysis/special_functions/trigonometric/angle.lean
chore(analysis): move `real.angle` to a dedicated file (#10065) …
Modified real.angleView on Github →
2019-10-03 17:37
src/analysis/complex/exponential.lean
chore(*): fix errors in library and sanity_check (#1499) …
Added real.angleView on Github →