Fungrim entry: c01d22

\mathbb{Q} = \left\{ \frac{p}{q} : p \in \mathbb{Z} \;\mathbin{\operatorname{and}}\; q \in \mathbb{Z} \setminus \left\{0\right\} \right\}

TeX:

\mathbb{Q} = \left\{ \frac{p}{q} : p \in \mathbb{Z} \;\mathbin{\operatorname{and}}\; q \in \mathbb{Z} \setminus \left\{0\right\} \right\}

Definitions:

Fungrim symbol	Notation	Short description
`QQ`	$\mathbb{Q}$	Rational numbers
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("c01d22"),
    Formula(Equal(QQ, Set(Div(p, q), For(Tuple(p, q)), And(Element(p, ZZ), Element(q, SetMinus(ZZ, Set(0))))))))

Topics using this entry

2021-03-15 19:12:00.328586 UTC