Fungrim home page

Fungrim entry: 4f0049

x+yi=x2+y2\left|x + y i\right| = \sqrt{{x}^{2} + {y}^{2}}
Assumptions:xR  and  yRx \in \mathbb{R} \;\mathbin{\operatorname{and}}\; y \in \mathbb{R}
TeX:
\left|x + y i\right| = \sqrt{{x}^{2} + {y}^{2}}

x \in \mathbb{R} \;\mathbin{\operatorname{and}}\; y \in \mathbb{R}
Definitions:
Fungrim symbol Notation Short description
Absz\left|z\right| Absolute value
ConstIii Imaginary unit
Sqrtz\sqrt{z} Principal square root
Powab{a}^{b} Power
RRR\mathbb{R} Real numbers
Source code for this entry:
Entry(ID("4f0049"),
    Formula(Equal(Abs(Add(x, Mul(y, ConstI))), Sqrt(Add(Pow(x, 2), Pow(y, 2))))),
    Variables(x, y),
    Assumptions(And(Element(x, RR), Element(y, RR))))

Topics using this entry

Copyright (C) Fredrik Johansson and contributors. Fungrim is provided under the MIT license. The source code is on GitHub.

2021-03-15 19:12:00.328586 UTC