Je vais tenter de lire cette démonstration très soigneusement. Le point délicat est que le Frido n'accepte que des références vers le haut; autrement dit, aucun résultat n'utilisant d'Alembert ne peut être utilisé avant d'avoir démontré d'Alembert.
Du coup, si on utilise quelque chose comme la forme trigonométrique des nombres complexes, ça risque de faire bouger énormément de résultats.
C'est une des raisons pour lesquelles j'ai pour l'instant décidé de mettre ce théorème avec Galois (rien que des choses pas démontrées) parce que j'ai une certaine certitude que la démonstration par ce biais est sans "dépendances" : il y a seulement des corps, des groupes et des extensions.
[^] # Re: L'analyse au delà de l'agrégation
Posté par LaurentClaessens (site web personnel) . En réponse à la dépêche Le Frido 2018, livre libre de mathématique pour l’agrégation. Évalué à 3.
Je vais tenter de lire cette démonstration très soigneusement. Le point délicat est que le Frido n'accepte que des références vers le haut; autrement dit, aucun résultat n'utilisant d'Alembert ne peut être utilisé avant d'avoir démontré d'Alembert.
Du coup, si on utilise quelque chose comme la forme trigonométrique des nombres complexes, ça risque de faire bouger énormément de résultats.
C'est une des raisons pour lesquelles j'ai pour l'instant décidé de mettre ce théorème avec Galois (rien que des choses pas démontrées) parce que j'ai une certaine certitude que la démonstration par ce biais est sans "dépendances" : il y a seulement des corps, des groupes et des extensions.