Fungrim home page

Fungrim entry: 148f96

z∈C[[x]]    ⟹    (ez∈C[[x]]  and⁡  [x0]ez≠0)z \in \mathbb{C}[[x]] \;\implies\; \left({e}^{z} \in \mathbb{C}[[x]] \;\mathbin{\operatorname{and}}\; [{x}^{0}] {e}^{z} \ne 0\right)
TeX:
z \in \mathbb{C}[[x]] \;\implies\; \left({e}^{z} \in \mathbb{C}[[x]] \;\mathbin{\operatorname{and}}\; [{x}^{0}] {e}^{z} \ne 0\right)
Definitions:
Fungrim symbol Notation Short description
PowerSeriesK[[x]]K[[x]] Formal power series
CCC\mathbb{C} Complex numbers
Expez{e}^{z} Exponential function
Source code for this entry:
Entry(ID("148f96"),
    Formula(Implies(Element(z, PowerSeries(CC, SerX)), And(Element(Exp(z), PowerSeries(CC, SerX)), NotEqual(Coefficient(Exp(z), SerX, 0), 0)))),
    Variables(z))

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