Construction des réels - l'ensemble quotient mérite une clarification

[ColinPitrat]

Dans la construction des réels (1.8 Les réels), j'ai des difficultés à comprendre le Théorème-définition 1.95 (L'anneau des réels).

Le théorème introduit l'ensemble quotient E/E0, ce qui nécessite d'être familier avec l'ensemble quotient d'un anneau par un de ses idéaux bilatères. Je pense qu'un petit rappel avant serait le bienvenu.

[LaurentClaessens]

Si ça se trouve, une partie de la preuve et de l'énoncé sont inutiles parce qu'il y aurait un résultat automatique pour le quotient d'un anneau par un idéal.

Et si ça se trouve, un tel résultat est déjà prouvé plus bas.

À voir...

[LaurentClaessens]

J'ai remonté la proposition qui dit qu'un quotien d'un anneau par un idéal est un anneau. J'ai aussi donné la définition d'un ensemble quotient par une relation d'équivalence.