Formaliser la preuve des traces
La preuve est pour le moment encore au stade informel
. Il faut regarder précisément les constantes, et prouver formellement (comme dans boustrophédon) l'injectivité de la fonction.
-
Donner une définition précise de la trace -
Faire proprement le lemme de panache
-
Montrer effectivement l'injectivité (en utilisant les idées du pdf dans le dossier ressources)
/estimate 0d 3h
Edited by Aliaume Lopez