959 B
up::arithmétique #s/maths/arithmétique
[!definition] divisibilité Soient
(a,b)\in\mathbb{Z}^2, on dit quebdivise $a$ et on note\boxed{b\mid a}s'il existeq\in\mathbb{Z}tel queb = aq^definition
Propriétés
[!proposition]+ fonction 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éfinird|ppar cas à partir deqcomme suit :d|p := \begin{cases} 1 \text{ si } p = d \times q(p, d) \\ 0 \text{ sinon}\end{cases}(prédicat "ddivise $p$") avecq(p, d) = \mu t \leq p \quad (p \dot{-} (td) < d)(quotient pour la division euclidienne deppard) (voir schéma mu borné) ^recursive-primitive