Documentation
APAP
.
Mathlib
.
Analysis
.
SpecialFunctions
.
Complex
.
Circle
Search
return to top
source
Imports
Init
Mathlib.Analysis.SpecialFunctions.Complex.Circle
Imported by
Circle
.
arg_eq_zero
source
@[simp]
theorem
Circle
.
arg_eq_zero
{
z
:
Circle
}
:
(↑
z
)
.
arg
=
0
↔
z
=
1