Assumptions:
TeX:
\log\!\left(\overline{z}\right) = \overline{\log(z)} z \in \mathbb{C} \setminus \left(-\infty, 0\right]
Definitions:
Fungrim symbol | Notation | Short description |
---|---|---|
Log | Natural logarithm | |
Conjugate | Complex conjugate | |
CC | Complex numbers | |
OpenClosedInterval | Open-closed interval | |
Infinity | Positive infinity |
Source code for this entry:
Entry(ID("13895b"), Formula(Equal(Log(Conjugate(z)), Conjugate(Log(z)))), Variables(z), Assumptions(Element(z, SetMinus(CC, OpenClosedInterval(Neg(Infinity), 0)))))