up::[[arithmétique]]
#s/maths/arithmétique


> [!definition] [[divisibilité]]
> Soient $(a,b)\in\mathbb{Z}^2$, on dit que **$b$ divise $a$** et on note $\boxed{b\mid a}$ s'il existe $q\in\mathbb{Z}$ tel que $b = aq$
^definition

# Propriétés

> [!proposition]+ [[fonction récursive primitive|récursive primitive]]
> Le prédicat de divisibilité est une [[fonction récursive primitive]]
> > [!démonstration]- Démonstration
> > Pour en faire un prédicat, on peut noter $d | q := \begin{cases} 1 \text{ si } d \text{ divise } q\\ 0 \text{ sinon} \end{cases}$
> > On peut alors définir $d|p$ par cas à partir de $q$ comme suit :
> > $d|p := \begin{cases} 1 \text{ si } p = d \times q(p, d) \\ 0 \text{ sinon}\end{cases}$  (prédicat "$d$ divise $p$")
> > avec $q(p, d) = \mu t \leq p \quad (p \dot{-} (td) < d)$  (quotient pour la division euclidienne de $p$ par $d$) (voir [[schéma mu borné|schéma µ borné]])
^recursive-primitive

# Exemples