Fungrim entry: 0d82d4

z \in \mathbb{R}[[x]] \;\implies\; \left({e}^{z} \in \mathbb{R}[[x]] \;\mathbin{\operatorname{and}}\; [{x}^{0}] {e}^{z} \ne 0\right)

TeX:

z \in \mathbb{R}[[x]] \;\implies\; \left({e}^{z} \in \mathbb{R}[[x]] \;\mathbin{\operatorname{and}}\; [{x}^{0}] {e}^{z} \ne 0\right)

Definitions:

Fungrim symbol	Notation	Short description
`PowerSeries`	$K[[x]]$	Formal power series
`RR`	$\mathbb{R}$	Real numbers
`Exp`	${e}^{z}$	Exponential function

Source code for this entry:

Entry(ID("0d82d4"),
    Formula(Implies(Element(z, PowerSeries(RR, SerX)), And(Element(Exp(z), PowerSeries(RR, SerX)), NotEqual(Coefficient(Exp(z), SerX, 0), 0)))),
    Variables(z))

Topics using this entry

Exponential function

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