Fungrim entry: 71a0b8

{e}^{\alpha} \notin \mathbb{Q} \;\text{ for all } \alpha \in \mathbb{Q} \setminus \left\{0\right\}

TeX:

{e}^{\alpha} \notin \mathbb{Q} \;\text{ for all } \alpha \in \mathbb{Q} \setminus \left\{0\right\}

Definitions:

Fungrim symbol	Notation	Short description
`Exp`	${e}^{z}$	Exponential function
`QQ`	$\mathbb{Q}$	Rational numbers

Source code for this entry:

Entry(ID("71a0b8"),
    Formula(All(NotElement(Exp(alpha), QQ), ForElement(alpha, SetMinus(QQ, Set(0))))))

Topics using this entry

2021-03-15 19:12:00.328586 UTC