Résumé :
Dans cette note nous examinons le théorème d'Artin en
théorie
de Galois et sa version "anneaux commutatifs".
Nous montrons comment décrypter certaines preuves classiques
usuelles
(qui utilisent le principe du tiers exclu et l'axiome du choix)
en des preuves constructives.
Il s'agit ici d'un "cas d'école" pour le décryptage des
preuves classiques, dans la mesure où une preuve constructive
élémentaire du théorème le plus fort peut
être
obtenue de façon beaucoup plus directe
(voir section 3).
Abstract :
We examine Artin's Theorem in Galois Theory and its commutative ring
version.
We show how to decipher some classical proofs (using Choice and
Third Excluded Middle) in order to get fully constructive results.
This is a study case because a direct and much shorter proof of the
main theorem is also given in section 3.