x divise y utilisé avant sa définition

[ColinPitrat]

Le concept de "A divise B" est utilisé dans la définition 1.46 de PPCM et PGCD, avant sa définition qui arrive en 1.51.

Si je comprends bien l'esprit du Frido, il faudrait déplacer la définition de PPCM et PGCD après la définition 1.51 ? Si c'est le cas, je peux envoyer une PR pour le faire.

D'autre part, la définition 1.46 mentionne:

Nous disons que µ dans A est un PPCM de S si (1) S | µ, (2) si S | m, alors µ | m. où S est un sous-ensemble de A et µ et m des éléments de A.

Du coup il me semble qu'il faudrait plutôt:

Nous disons que µ dans A est un PPCM de S si (1) pour tout n dans S, n | µ, (2) si pour tout n dans S, n | m, alors µ | m. Ou bien la notation utilisée est-elle d'usage?

[ColinPitrat]

Après avoir été un peu plus loin dans ma lecture du Frido, il me semble que la contrainte de ne pas faire de référence vers l'avant est surtout appliquée aux démonstrations et est moins contraignante pour les définitions.

Je ferme donc ce ticket. J'envoi une PR pour la reformulation du PPCM.