diff --git a/MyIA.AI.Notebooks/GameTheory/GameTheory-23b-Lean-Assignment-Native.ipynb b/MyIA.AI.Notebooks/GameTheory/GameTheory-23b-Lean-Assignment-Native.ipynb index ff135f7314..6566c8c394 100644 --- a/MyIA.AI.Notebooks/GameTheory/GameTheory-23b-Lean-Assignment-Native.ipynb +++ b/MyIA.AI.Notebooks/GameTheory/GameTheory-23b-Lean-Assignment-Native.ipynb @@ -1581,7 +1581,10 @@ "source": [ "-- Exercice 1 (Definitions) : votre propre matrice 2x2.\n", "-- Construire une matrice C2 : Fin 2 → Fin 2 → ℤ dont l'affectation optimale\n", - "-- N'EST PAS l'identite (la transposition gagne : [[1, 0], [0, 1]] → swap = 0, id = 2).\n", + "-- N'EST PAS l'identité (la matrice [[1, 0], [0, 1]] en est un bon\n", + "-- prototype : identité de coût 2 mais transposition de coût 0, donc\n", + "-- l'optimum est la TRANSPOSITION (Equiv.swap) — exactement ce qu'on\n", + "-- cherche à faire surgir dans le théorème optimal_C2 ci-dessous).\n", "--\n", "-- Etape 1 : definir C2 avec la notation ![![.., ..], ![.., ..]].\n", "-- Etape 2 : #eval Assignment.value C2 sur Equiv.refl _ et (Equiv.swap (0 : Fin 2) 1).\n",