fix

affeldt-aist · Feb 2, 2024 · 2c56f7b · 2c56f7b
1 parent d7fb95c
commit 2c56f7b
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/probability/convex_equiv.v b/probability/convex_equiv.v
@@ -554,7 +554,7 @@ Lemma axinjmap : ax_inj_map T.
 Proof.
 move=> n m u d g Hu.
 have -> : fdistmap u d = fdist_convn d (fun i : 'I_m => fdist1 (u i)).
-  by apply fdist_ext => i; rewrite /fdistmap fdistbindE fdist_convnE.
+  by apply fdist_ext => i; rewrite /fdistmap fdistbindE// fdist_convnE.
 rewrite -axbarypart.
 - congr (<&>_ _ _); apply funext => j /=; symmetry; apply axidem => i.
   by rewrite supp_fdist1 inE => /eqP ->.