Assumptions:
TeX:
\chi(0) = \begin{cases} 1, & q = 1\\0, & q \ne 1\\ \end{cases}
q \in \mathbb{Z}_{\ge 1} \;\mathbin{\operatorname{and}}\; \chi \in G_{q}Definitions:
| Fungrim symbol | Notation | Short description |
|---|---|---|
| ZZGreaterEqual | Integers greater than or equal to n | |
| DirichletGroup | Dirichlet characters with given modulus |
Source code for this entry:
Entry(ID("458198"),
Formula(Equal(chi(0), Cases(Tuple(1, Equal(q, 1)), Tuple(0, NotEqual(q, 1))))),
Variables(q, chi),
Assumptions(And(Element(q, ZZGreaterEqual(1)), Element(chi, DirichletGroup(q)))))