Assumptions:
TeX:
\operatorname{Im}\!\left(x + y i\right) = y
x \in \mathbb{R} \;\mathbin{\operatorname{and}}\; y \in \mathbb{R}Definitions:
| Fungrim symbol | Notation | Short description |
|---|---|---|
| Im | Imaginary part | |
| ConstI | Imaginary unit | |
| RR | Real numbers |
Source code for this entry:
Entry(ID("ba6d81"),
Formula(Equal(Im(Add(x, Mul(y, ConstI))), y)),
Variables(x, y),
Assumptions(And(Element(x, RR), Element(y, RR))))