Merge pull request #93 from affeldt-aist/sub_vec

Change the notation for `sub_vec` from `#` to `\#`
affeldt-aist · Dec 13, 2022 · 8a67187 · 8a67187
2 parents f5057ac + 5842ecd
commit 8a67187
Show file tree

Hide file tree

Showing 4 changed files with 39 additions and 39 deletions.
diff --git a/ecc_modern/ldpc.v b/ecc_modern/ldpc.v
@@ -126,8 +126,8 @@ Local Notation "''F'" := (Fnext H).
 Variable tanner : Tanner.acyclic_graph (tanner_rel H).
 
 Lemma DMC_sub_vec_Fnext t n0 :
-  W ``(tb # [set~ n0] | t # [set~ n0]) =
-  (\prod_(i in 'F n0) W ``(tb # 'V(i, n0) :\ n0 | t # 'V(i, n0) :\ n0))%R.
+  W ``(tb \# [set~ n0] | t \# [set~ n0]) =
+  (\prod_(i in 'F n0) W ``(tb \# 'V(i, n0) :\ n0 | t \# 'V(i, n0) :\ n0))%R.
 Proof.
 rewrite DMCE.
 transitivity (\prod_(i in setT :\ n0) W (t ``_ i) (tb ``_ i))%R.
@@ -188,9 +188,9 @@ by rewrite DMCE -rprod_sub_vec.
 Qed.
 
 Lemma DMC_sub_vec_Vgraph t m0 n0 : n0 \in 'V m0 ->
-   W ``(tb # ('V(m0, n0) :\ n0) | t # ('V(m0, n0) :\ n0)) =
+   W ``(tb \# ('V(m0, n0) :\ n0) | t \# ('V(m0, n0) :\ n0)) =
    (\prod_(n1 in 'V m0 :\ n0) (W (t ``_ n1) (tb ``_ n1) *
-     \prod_(m1 in 'F n1 :\ m0) W ``(tb # 'V(m1, n1) :\ n1 | t # 'V(m1, n1) :\ n1)))%R.
+     \prod_(m1 in 'F n1 :\ m0) W ``(tb \# 'V(m1, n1) :\ n1 | t \# 'V(m1, n1) :\ n1)))%R.
 Proof.
 move=> m0n0.
 rewrite DMCE rprod_sub_vec.
@@ -248,7 +248,7 @@ Variable y : 'rV[B]_n.
 Local Open Scope R_scope.
 
 Definition alpha m0 n0 d := \sum_(x = d [~'V(m0, n0) :\ n0])
-  W ``(y # 'V(m0, n0) :\ n0 | x # 'V(m0, n0) :\ n0) *
+  W ``(y \# 'V(m0, n0) :\ n0 | x \# 'V(m0, n0) :\ n0) *
     \prod_(m1 in 'F(m0, n0)) (\delta ('V m1) x)%:R.
 
 Definition beta n0 m0 (d : 'rV_n) :=
@@ -267,15 +267,15 @@ Proof.
 move=> n0m0 dd'.
 rewrite /alpha.
 transitivity (\sum_(x = d [~'V(m0, n0) :\ n0])
-     W ``((y # 'V(m0, n0) :\ n0) | ((dproj_V m0 n0 d x) # 'V(m0, n0) :\ n0)) *
+     W ``((y \# 'V(m0, n0) :\ n0) | ((dproj_V m0 n0 d x) \# 'V(m0, n0) :\ n0)) *
      (\prod_(m2 in 'F(m0, n0)) (\delta ('V m2) (dproj_V m0 n0 d x))%:R))%R.
   apply eq_bigr => /= t Ht.
   congr (W ``(_ | _) * _)%R.
     by rewrite /dproj_V sub_vec_dproj.
   apply eq_bigr => i Hi.
   by rewrite /dproj_V checksubsum_dproj_freeon.
 transitivity (\sum_(x = d [~'V(m0, n0) :\ n0])
-     W ``((y # 'V(m0, n0) :\ n0) | ((dproj_V m0 n0 d' x) # 'V(m0, n0) :\ n0)) *
+     W ``((y \# 'V(m0, n0) :\ n0) | ((dproj_V m0 n0 d' x) \# 'V(m0, n0) :\ n0)) *
      (\prod_(m2 in 'F(m0, n0)) (\delta ('V m2) (dproj_V m0 n0 d' x))%:R))%R.
   apply eq_bigr => /= i Hi.
   congr (W ``(_ | _) * _)%R.
@@ -295,7 +295,7 @@ transitivity (\sum_(x = d [~'V(m0, n0) :\ n0])
   move: kn0.
   by apply Fgraph_Vnext_Vgraph with j.
 transitivity (\sum_(x = d' [~'V(m0, n0) :\ n0])
-     W ``((y # 'V(m0, n0) :\ n0) | ((dproj_V m0 n0 d' x) # 'V(m0, n0) :\ n0)) *
+     W ``((y \# 'V(m0, n0) :\ n0) | ((dproj_V m0 n0 d' x) \# 'V(m0, n0) :\ n0)) *
      (\prod_(m2 in 'F(m0, n0)) (\delta ('V m2) (dproj_V m0 n0 d' x))%:R))%R; last first.
    apply/esym.
    apply eq_bigr => /= t Ht.
@@ -338,15 +338,15 @@ Proof.
 move=> n0m0 dd' Hm1.
 rewrite /alpha.
 transitivity (\sum_(x = d [~'V(m1, n0) :\ n0])
-      W ``((y # 'V(m1, n0) :\ n0) | ((dproj_V m1 n0 d x) # 'V(m1, n0) :\ n0)) *
+      W ``((y \# 'V(m1, n0) :\ n0) | ((dproj_V m1 n0 d x) \# 'V(m1, n0) :\ n0)) *
       (\prod_(m2 in 'F(m1, n0)) (\delta ('V m2) (dproj_V m1 n0 d x))%:R))%R.
   apply eq_bigr => /= t Ht.
   congr (W ``(_ | _) * _)%R.
     by rewrite /dproj_V sub_vec_dproj.
   apply eq_bigr => i Hi.
   by rewrite checksubsum_dproj_freeon.
 transitivity (\sum_(x = d [~'V(m1, n0) :\ n0])
-      W ``((y # 'V(m1, n0) :\ n0) | ((dproj_V m1 n0 d' x) # 'V(m1, n0) :\ n0)) *
+      W ``((y \# 'V(m1, n0) :\ n0) | ((dproj_V m1 n0 d' x) \# 'V(m1, n0) :\ n0)) *
       (\prod_(m2 in 'F(m1, n0)) (\delta ('V m2) (dproj_V m1 n0 d' x))%:R))%R.
   apply eq_bigr => /= i Hi.
   congr (W ``(_ | _) * _)%R.
@@ -366,7 +366,7 @@ transitivity (\sum_(x = d [~'V(m1, n0) :\ n0])
   move: kn0.
   by apply Fgraph_Vnext_Vgraph with j.
 transitivity (\sum_(x = d' [~'V(m1, n0) :\ n0])
-      W ``((y # 'V(m1, n0) :\ n0) | ((dproj_V m1 n0 d' x) # 'V(m1, n0) :\ n0)) *
+      W ``((y \# 'V(m1, n0) :\ n0) | ((dproj_V m1 n0 d' x) \# 'V(m1, n0) :\ n0)) *
       (\prod_(m2 in 'F(m1, n0)) (\delta ('V m2) (dproj_V m1 n0 d' x))%:R))%R; last first.
     apply/esym.
     apply eq_bigr => /= t Ht.
@@ -464,7 +464,7 @@ transitivity (post_prob_uniform_cst [set cw in C] y *
   by rewrite checksubsum_in_kernel inE mem_kernel_syndrome0.
 congr (_ * _)%R.
 transitivity (W `(y ``_ n0 | b) *
-  (\sum_(x = d [~ setT :\ n0]) W ``(y # ~: [set n0] | x # ~: [set n0]) *
+  (\sum_(x = d [~ setT :\ n0]) W ``(y \# ~: [set n0] | x \# ~: [set n0]) *
    \prod_(m0 < m) (\delta ('V m0) x)%:R)).
   rewrite big_distrr /=; apply eq_bigr => t Ht.
   rewrite mulRA; congr (_ * _)%R.
@@ -474,15 +474,15 @@ transitivity (W `(y ``_ n0 | b) *
   by rewrite in_setC in_set1.
 congr (_ * _).
 transitivity (
-    \sum_(x = d [~ setT :\ n0]) W ``(y # ~: [set n0] | x # ~: [set n0]) *
+    \sum_(x = d [~ setT :\ n0]) W ``(y \# ~: [set n0] | x \# ~: [set n0]) *
     \prod_(m0 in 'F n0) \prod_(m1 in 'F(m0, n0)) (\delta ('V m1) x)%:R).
   apply eq_bigr => /= t Ht.
   congr (_ * _)%R.
   by rewrite -(rprod_Fgraph_part_fnode (Tanner.connected tanner) (Tanner.acyclic tanner)
       (fun m0 => (\delta ('V m0) t)%:R)).
 transitivity (
   \sum_(x = d [~ setT :\ n0]) \prod_(m0 in 'F n0)
-    (W ``(y # 'V(m0, n0) :\ n0 | x # 'V(m0, n0) :\ n0) *
+    (W ``(y \# 'V(m0, n0) :\ n0 | x \# 'V(m0, n0) :\ n0) *
       \prod_(m1 in 'F(m0, n0)) (\delta ('V m1) x)%:R)).
   apply eq_bigr => /= t Ht.
   rewrite [in X in _ = X]big_split /=; congr (_ * _).
@@ -533,12 +533,12 @@ rewrite /alpha.
 transitivity (W Zp0 (y ``_ n0) *
   (\sum_(ta = df `[ n0 := Zp0 ] [~ setT :\ n0])
     \prod_(m1 in 'F n0)
-      (W ``(y # 'V(m1, n0) :\ n0 | ta # 'V(m1, n0) :\ n0) *
+      (W ``(y \# 'V(m1, n0) :\ n0 | ta \# 'V(m1, n0) :\ n0) *
       (\prod_(m2 in 'F(m1, n0)) (\delta ('V m2) ta)%:R))) +
   W Zp1 (y ``_ n0) *
   (\sum_(ta = df `[ n0 := Zp1 ] [~ setT :\ n0])
     \prod_(m1 in 'F n0)
-      (W ``(y # 'V(m1, n0) :\ n0 | ta # 'V(m1, n0) :\ n0) *
+      (W ``(y \# 'V(m1, n0) :\ n0 | ta \# 'V(m1, n0) :\ n0) *
       (\prod_(m2 in 'F(m1, n0)) (\delta ('V m2) ta)%:R)))).
   congr (_ * _ + _ * _).
     rewrite (rmul_rsum_commute0 (Tanner.connected tanner) (Tanner.acyclic tanner) y
@@ -549,7 +549,7 @@ transitivity (W Zp0 (y ``_ n0) *
   by rewrite checksubsum_dprojs_V.
 transitivity (\sum_(ta : 'rV_n) W (ta ``_ n0) (y ``_ n0) *
     \prod_(m1 in 'F n0)
-      (W ``(y # 'V(m1, n0) :\ n0 | ta # 'V(m1, n0) :\ n0) *
+      (W ``(y \# 'V(m1, n0) :\ n0 | ta \# 'V(m1, n0) :\ n0) *
         (\prod_(m2 in 'F(m1, n0)) (\delta ('V m2) ta)%:R))).
   rewrite big_distrr big_distrr /=.
   rewrite [in X in _ = X] (bigID [pred x : 'rV_n | x ``_ n0 == Zp0]) /=.
@@ -563,7 +563,7 @@ transitivity (\sum_(ta : 'rV_n) W (ta ``_ n0) (y ``_ n0) *
       by rewrite -F2_eq1 => /eqP ->.
     move=> v /=; by rewrite -freeon_all mxE eqxx F2_eq1.
 transitivity (\sum_(ta : 'rV_n) W (ta ``_ n0) (y ``_ n0) *
-    (\prod_(m1 in 'F n0) W ``(y # 'V(m1, n0) :\ n0 | ta # 'V(m1, n0) :\ n0)) *
+    (\prod_(m1 in 'F n0) W ``(y \# 'V(m1, n0) :\ n0 | ta \# 'V(m1, n0) :\ n0)) *
     (\prod_(m1 in 'F n0) (\prod_(m2 in 'F(m1, n0)) (\delta ('V m2) ta)%:R))).
   apply eq_bigr => ta _.
   rewrite -mulRA.
@@ -633,7 +633,7 @@ Lemma recursive_computation_helper m0 n0 d : n0 \in 'V m0 ->
           \prod_(n1 < n | n1 \in 'V m0 :\ n0)
              ((W i ``_ n1) y ``_ n1 *
              (\prod_(m1 < m | m1 \in 'F n1 :\ m0)
-                 (W ``((y # 'V( m1, n1) :\ n1) | (i # 'V( m1, n1) :\ n1)) *
+                 (W ``((y \# 'V( m1, n1) :\ n1) | (i \# 'V( m1, n1) :\ n1)) *
                  (\prod_(m2 < m | m2 \in 'F( m1, n1)) (\delta ('V m2) i)%:R)))) in
   A = \prod_(n1 < n | n1 \in 'V m0 :\ n0) beta n1 m0 x.
  Proof.
@@ -643,7 +643,7 @@ transitivity (\prod_(n1 in 'V m0 :\ n0) ((W x ``_ n1) y ``_ n1 *
       pfamily x ('F n1 :\ m0) (fun m1 => freeon ('V( m1, n1) :\ n1) x)) &&
       (comb_V H x n1 (dprojs_V H x n1 z) == z))
     \prod_(m1 in 'F n1 :\ m0)
-      (W ``((y # 'V( m1, n1) :\ n1) | ((dprojs_V H x n1 z) m1 # 'V( m1, n1) :\ n1)) *
+      (W ``((y \# 'V( m1, n1) :\ n1) | ((dprojs_V H x n1 z) m1 \# 'V( m1, n1) :\ n1)) *
         (\prod_(m2 in 'F( m1, n1)) (\delta ('V m2) ((dprojs_V H x n1 z) m1))%:R))))).
   apply eq_bigr => n1 Hn1.
   congr (_ * _)%R.
@@ -657,7 +657,7 @@ transitivity (\prod_(n1 in 'V m0 :\ n0)
       (comb_V H x n1 (dprojs_V H x n1 z) == z))
     (W z ``_ n1) y ``_ n1 *
     (\prod_(m1 in 'F n1 :\ m0)
-        (W ``((y # 'V( m1, n1) :\ n1) | ((dprojs_V H x n1 z) m1 # 'V( m1, n1) :\ n1)) *
+        (W ``((y \# 'V( m1, n1) :\ n1) | ((dprojs_V H x n1 z) m1 \# 'V( m1, n1) :\ n1)) *
          (\prod_(m2 in 'F( m1, n1)) (\delta ('V m2) ((dprojs_V H x n1 z) m1))%:R)))).
   apply/esym.
   apply eq_bigr => /= n1 Hn1.
@@ -675,7 +675,7 @@ transitivity (\sum_(t | (dprojs_V2 H x m0 n0 t \in
     \prod_(n1 < n | n1 \in 'V m0 :\ n0)
       (W (((dprojs_V2 H x m0 n0 t) n1) ``_ n1) y ``_ n1 *
       (\prod_(m1 < m | m1 \in 'F n1 :\ m0)
-        (W ``((y # 'V( m1, n1) :\ n1) | ((dprojs_V H x n1 ((dprojs_V2 H x m0 n0 t) n1)) m1 # 'V( m1, n1) :\ n1)) *
+        (W ``((y \# 'V( m1, n1) :\ n1) | ((dprojs_V H x n1 ((dprojs_V2 H x m0 n0 t) n1)) m1 \# 'V( m1, n1) :\ n1)) *
         (\prod_(m2 < m | m2 \in 'F( m1, n1))
           (\delta ('V m2) ((dprojs_V H x n1 ((dprojs_V2 H x m0 n0 t) n1)) m1))%:R))))).
   apply/esym.
@@ -717,7 +717,7 @@ Proof.
 move=> m0n0.
 transitivity (\sum_(x = d [~'V(m0, n0) :\ n0])
     (\delta ('V m0) x)%:R *
-      W ``(y # 'V(m0, n0) :\ n0 | x # 'V(m0, n0) :\ n0) * \prod_(n1 in 'V m0 :\ n0) \prod_(m1 in 'F n1 :\ m0) \prod_(m2 in 'F(m1, n1))
+      W ``(y \# 'V(m0, n0) :\ n0 | x \# 'V(m0, n0) :\ n0) * \prod_(n1 in 'V m0 :\ n0) \prod_(m1 in 'F n1 :\ m0) \prod_(m2 in 'F(m1, n1))
          (\delta ('V m2) x)%:R).
   (* get W(tb|t) out of beta *)
   rewrite /alpha.
@@ -754,7 +754,7 @@ transitivity (\sum_(x = d [~'V(m0, n0) :\ n0])
   (\delta ('V m0) x)%:R *
     \prod_(n1 in 'V m0 :\ n0) (W `(y ``_ n1 | x ``_ n1) *
     \prod_(m1 in 'F n1 :\ m0)
-     ((W ``(y # 'V(m1, n1) :\ n1 | x # 'V(m1, n1) :\ n1))
+     ((W ``(y \# 'V(m1, n1) :\ n1 | x \# 'V(m1, n1) :\ n1))
       * \prod_(m2 in 'F(m1, n1)) (\delta ('V m2) x)%:R))).
   apply eq_bigr => /= t Ht.
   rewrite -mulRA; congr (_ * _).
@@ -767,7 +767,7 @@ transitivity (\sum_(x = d [~('V m0) :\ n0])
     \prod_(n1 in 'V m0 :\ n0)
       (W (x' ``_ n1) (y ``_ n1) *
       (\prod_(m1 in 'F n1 :\ m0)
-          (W ``(y # 'V(m1, n1) :\ n1 | x' # 'V(m1, n1) :\ n1) *
+          (W ``(y \# 'V(m1, n1) :\ n1 | x' \# 'V(m1, n1) :\ n1) *
           (\prod_(m2 in 'F(m1, n1)) (\delta ('V m2) x')%:R))))).
   apply partition_big => /= t _.
   by apply freeon_dproj.
@@ -777,7 +777,7 @@ transitivity
   (\delta ('V m0) x)%:R *
   (\prod_(n1 in 'V m0 :\ n0) (W (x' ``_ n1) y ``_ n1 *
     (\prod_(m1 in 'F n1 :\ m0)
-      (W ``(y # 'V(m1, n1) :\ n1 | x' # 'V(m1, n1) :\ n1) *
+      (W ``(y \# 'V(m1, n1) :\ n1 | x' \# 'V(m1, n1) :\ n1) *
         (\prod_(m2 in 'F(m1, n1)) (\delta ('V m2) x')%:R)))))).
   apply eq_bigr => /= x' Hx'.
   congr (_%:R * _)%R.

diff --git a/ecc_modern/summary_tanner.v b/ecc_modern/summary_tanner.v
@@ -38,7 +38,7 @@ Implicit Types A : finType.
 Definition dproj d s t :=
   locked (\row_(j < n) if j \in s then t ``_ j else d ``_ j).
 
-Lemma sub_vec_dproj d t s' s : s \subset s' -> (dproj d s' t) # s = t # s.
+Lemma sub_vec_dproj d t s' s : s \subset s' -> (dproj d s' t) \# s = t \# s.
 Proof.
 move=> s's.
 rewrite /dproj; unlock; apply/rowP => i; rewrite !mxE; case: ifPn => //.
@@ -73,7 +73,7 @@ Definition dprojs d A (g : A -> {set 'I_n}) t :=
   locked [ffun a => dproj d (g a) t].
 
 Lemma sub_vec_dprojs d t A (g : A -> {set 'I_n}) s a :
-  s \subset g a -> ((dprojs d g t) a) # s = t # s.
+  s \subset g a -> ((dprojs d g t) a) \# s = t \# s.
 Proof. rewrite /dprojs; unlock => H0; by rewrite ffunE sub_vec_dproj. Qed.
 
 Lemma freeon_dprojs d t A (g : A -> {set 'I_n}) a : freeon (g a) d ((dprojs d g t) a).
@@ -295,9 +295,9 @@ Lemma rmul_rsum_commute0 d n0 (B : finType) (t : 'rV[B]_n)
   (F : 'I_m -> 'rV_n -> R)
   (HF : forall m1 m0 (t' : 'rV_n), m1 \in 'F(m0, n0) -> t' ``_ n0 = d ``_ n0 -> F m1 ((dprojs_V H d n0 t') m0) = F m1 t') :
   \prod_(m0 in 'F n0) (\sum_(t' = d [~'V(m0, n0) :\ n0])
-    W _ (t # 'V(m0, n0) :\ n0) (t' # 'V(m0, n0) :\ n0) * \prod_(m1 in 'F(m0, n0)) F m1 t') =
+    W _ (t \# 'V(m0, n0) :\ n0) (t' \# 'V(m0, n0) :\ n0) * \prod_(m1 in 'F(m0, n0)) F m1 t') =
   \sum_(t' = d [~ setT :\ n0]) (\prod_(m0 in 'F n0)
-    (W _ (t # 'V(m0, n0) :\ n0) (t' # 'V(m0, n0) :\ n0) * \prod_(m1 in 'F(m0, n0)) F m1 t')).
+    (W _ (t \# 'V(m0, n0) :\ n0) (t' \# 'V(m0, n0) :\ n0) * \prod_(m1 in 'F(m0, n0)) F m1 t')).
 Proof.
 rewrite (big_distr_big_dep d [pred x in 'F n0] (fun i => freeon ('V(i, n0) :\ n0) d)) [LHS]/=.
 rewrite (reindex_onto (dprojs_V H d n0) (comb_V H d n0)); last first.
@@ -344,7 +344,7 @@ Definition dprojs_V2 d m0 n0 t : {ffun 'I_n -> 'rV_n} := dprojs d (ssgraph m0 n0
 Definition comb_V2 d m0 n0 (f : {ffun 'I_n -> 'rV_n}) := comb d f (ssgraph m0 n0).
 
 Lemma sub_vec_dprojs_V2 d m0 n0 t n1 m1 : n1 \in 'V m0 :\ n0 -> m1 \in `F n1 :\ m0 ->
-  (dprojs_V2 d m0 n0 t) n1 # `V(m1, n1) :\ n1 = t # `V(m1, n1) :\ n1.
+  (dprojs_V2 d m0 n0 t) n1 \# `V(m1, n1) :\ n1 = t \# `V(m1, n1) :\ n1.
 Proof.
 move=> Hn1 Hm1; rewrite /dprojs_V2 sub_vec_dprojs //.
 apply/subsetP => n2 Hn2.
@@ -719,13 +719,13 @@ Lemma rprod_rsum_commute d (B : finType) (x : 'rV_n) (W: `Ch('F_2, B)) m0 n0 (m0
     (\sum_(t | pr n1 t)
       W (t ``_ n1) (x ``_ n1) *
          \prod_(m1 in `F n1 :\ m0)
-           (W ``(x # `V(m1, n1) :\ n1 | ((dprojs_V H d n1 t) m1) # `V(m1, n1) :\ n1) *
+           (W ``(x \# `V(m1, n1) :\ n1 | ((dprojs_V H d n1 t) m1) \# `V(m1, n1) :\ n1) *
              \prod_(m2 in `F(m1, n1)) INR (\delta ('V m2) ((dprojs_V H d n1 t) m1)))) =
   \sum_(t | (g t \in pfamily d ('V m0 :\ n0) pr) && (g' (g t) == t))
     \prod_(n1 in 'V m0 :\ n0)
        (W ((g t n1) ``_ n1) (x ``_ n1) *
          \prod_(m1 in `F n1 :\ m0)
-           (W ``(x # `V(m1, n1) :\ n1 | ((dprojs_V H d n1 (g t n1)) m1) # `V(m1, n1) :\ n1) *
+           (W ``(x \# `V(m1, n1) :\ n1 | ((dprojs_V H d n1 (g t n1)) m1) \# `V(m1, n1) :\ n1) *
              \prod_(m2 in `F(m1, n1)) INR (\delta ('V m2) ((dprojs_V H d n1 (g t n1)) m1)))))%R.
 Proof.
 move=> pr g g'.

diff --git a/information_theory/channel.v b/information_theory/channel.v
@@ -134,7 +134,7 @@ Section DMC_sub_vec.
 Variables (A B : finType) (W : `Ch(A, B)) (n : nat) (tb : 'rV[B]_n).
 
 Lemma rprod_sub_vec (D : {set 'I_n}) (t : 'rV_n) :
-  \prod_(i < #|D|) W ((t # D) ``_ i) ((tb # D) ``_ i) =
+  \prod_(i < #|D|) W ((t \# D) ``_ i) ((tb \# D) ``_ i) =
   \prod_(i in D) W (t ``_ i) (tb ``_ i).
 Proof.
 have [->|/set0Pn[i iD]] := eqVneq D set0.
@@ -154,7 +154,7 @@ by rewrite /f /=; case: Bool.bool_dec => [a| //]; rewrite enum_rankK_in.
 Qed.
 
 Lemma DMC_sub_vecE (V : {set 'I_n}) (t : 'rV_n) :
-  W ``(tb # V | t # V) = \prod_(i in V) W (t ``_ i) (tb ``_ i).
+  W ``(tb \# V | t \# V) = \prod_(i in V) W (t ``_ i) (tb ``_ i).
 Proof. by rewrite DMCE -rprod_sub_vec. Qed.
 
 End DMC_sub_vec.

diff --git a/lib/ssralg_ext.v b/lib/ssralg_ext.v
@@ -10,7 +10,7 @@ Require Import ssr_ext f2.
 (*  v ``_ i       == the ith element of v                                     *)
 (*  supp v        == the set of indices of elements from v that are not 0     *)
 (*  v `[ i := x ] == v where the ith element has been replaced with x         *)
-(*  v # S         == the vector of size #|S| containing the elements of       *)
+(*  v \# S        == the vector of size #|S| containing the elements of       *)
 (*                    index i \in S                                           *)
 (*                                                                            *)
 (* Section prod_rV:                                                           *)
@@ -34,7 +34,7 @@ Local Open Scope ring_scope.
 
 Notation "x '``_' i" := (x ord0 i) (at level 9) : vec_ext_scope.
 Reserved Notation "v `[ i := x ]" (at level 20).
-Reserved Notation "t # V" (at level 55, V at next level).
+Reserved Notation "t \# V" (at level 55, V at next level).
 
 Section AboutRingType.
 Variable R : ringType.
@@ -102,12 +102,12 @@ Section sub_vec_sect.
 Variables (A : Type) (n : nat).
 
 Definition sub_vec (t : 'rV[A]_n) (S : {set 'I_n}) : 'rV[A]_#| S | :=
-  \row_(j < #|S|) (t ``_ (enum_val j)).
+  \row_(j < #|S|) t ``_ (enum_val j).
 (* NB: enum_val j is the jth item of enum S *)
 
 End sub_vec_sect.
 
-Notation "t # S" := (sub_vec t S) : vec_ext_scope.
+Notation "t \# S" := (sub_vec t S) : vec_ext_scope.
 
 Section prod_rV.
 Variables A B : Type.