Fungrim home page

Fungrim entry: a807a7

(z∈Q[[x]]  and⁡  [x0]z=0)    ⟹    (ez∈Q[[x]]  and⁡  [x0]ez=1)\left(z \in \mathbb{Q}[[x]] \;\mathbin{\operatorname{and}}\; [{x}^{0}] z = 0\right) \;\implies\; \left({e}^{z} \in \mathbb{Q}[[x]] \;\mathbin{\operatorname{and}}\; [{x}^{0}] {e}^{z} = 1\right)
TeX:
\left(z \in \mathbb{Q}[[x]] \;\mathbin{\operatorname{and}}\; [{x}^{0}] z = 0\right) \;\implies\; \left({e}^{z} \in \mathbb{Q}[[x]] \;\mathbin{\operatorname{and}}\; [{x}^{0}] {e}^{z} = 1\right)
Definitions:
Fungrim symbol Notation Short description
PowerSeriesK[[x]]K[[x]] Formal power series
QQQ\mathbb{Q} Rational numbers
Expez{e}^{z} Exponential function
Source code for this entry:
Entry(ID("a807a7"),
    Formula(Implies(And(Element(z, PowerSeries(QQ, SerX)), Equal(Coefficient(z, SerX, 0), 0)), And(Element(Exp(z), PowerSeries(QQ, SerX)), Equal(Coefficient(Exp(z), SerX, 0), 1)))),
    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