Fungrim home page

Fungrim entry: ef9f8a

Symbol: Pow ab{a}^{b} Power
The following table lists conditions such that Pow(a, b) is defined in Fungrim.
Domain Codomain
aC0  and  bCa \in \mathbb{C} \setminus 0 \;\mathbin{\operatorname{and}}\; b \in \mathbb{C} abC{a}^{b} \in \mathbb{C}
aC  and  b{0}a \in \mathbb{C} \;\mathbin{\operatorname{and}}\; b \in \left\{0\right\} ab{1}{a}^{b} \in \left\{1\right\}
a{,,~}  and  b{1,2,}a \in \left\{\infty, -\infty, {\tilde \infty}\right\} \;\mathbin{\operatorname{and}}\; b \in \{-1, -2, \ldots\} ab{0}{a}^{b} \in \left\{0\right\}
General domains
aR  and  RRings  and  bZ0a \in R \;\mathbin{\operatorname{and}}\; R \in \operatorname{Rings} \;\mathbin{\operatorname{and}}\; b \in \mathbb{Z}_{\ge 0} abR{a}^{b} \in R
aK{0}  and  KFields  and  QK  and  bZa \in K \setminus \left\{0\right\} \;\mathbin{\operatorname{and}}\; K \in \operatorname{Fields} \;\mathbin{\operatorname{and}}\; \mathbb{Q} \subseteq K \;\mathbin{\operatorname{and}}\; b \in \mathbb{Z} abR{a}^{b} \in R
Table data: (P,Q)\left(P, Q\right) such that (P)    (Q)\left(P\right) \implies \left(Q\right)
Fungrim symbol Notation Short description
Powab{a}^{b} Power
CCC\mathbb{C} Complex numbers
Infinity\infty Positive infinity
UnsignedInfinity~{\tilde \infty} Unsigned infinity
ZZLessEqualZn\mathbb{Z}_{\le n} Integers less than or equal to n
ZZGreaterEqualZn\mathbb{Z}_{\ge n} Integers greater than or equal to n
QQQ\mathbb{Q} Rational numbers
ZZZ\mathbb{Z} Integers
Source code for this entry:
    SymbolDefinition(Pow, Pow(a, b), "Power"),
    Description("The following table lists conditions such that", SourceForm(Pow(a, b)), "is defined in Fungrim."),
    Table(TableRelation(Tuple(P, Q), Implies(P, Q)), TableHeadings(Description("Domain"), Description("Codomain")), List(TableSection("Numbers"), Tuple(And(Element(a, SetMinus(CC, 0)), Element(b, CC)), Element(Pow(a, b), CC)), Tuple(And(Element(a, CC), Element(b, Set(0))), Element(Pow(a, b), Set(1))), TableSection("Infinities"), Tuple(And(Element(a, Set(Infinity, Neg(Infinity), UnsignedInfinity)), Element(b, ZZLessEqual(-1))), Element(Pow(a, b), Set(0))), TableSection("General domains"), Tuple(And(Element(a, R), Element(R, Rings), Element(b, ZZGreaterEqual(0))), Element(Pow(a, b), R)), Tuple(And(Element(a, SetMinus(K, Set(0))), Element(K, Fields), SubsetEqual(QQ, K), Element(b, ZZ)), Element(Pow(a, b), R)))))

Topics using this entry

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

2020-04-08 16:14:44.404316 UTC