generalise path_entry_vector

Signed-off-by: Ali Caglayan <[email protected]>
HoTT · Jun 3, 2024 · fde5a49 · fde5a49
1 parent b312fba
commit fde5a49
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 3 deletions.
diff --git a/theories/Algebra/Rings/Matrix.v b/theories/Algebra/Rings/Matrix.v
@@ -360,7 +360,7 @@ Proof.
   rewrite kronecker_delta_symm.
   unfold kronecker_delta.
   destruct (dec (i = j)) as [p|np].
-  1: destruct p; f_ap; apply path_entry_vector.
+  1: f_ap; symmetry; by apply path_entry_vector.
   by rewrite !rng_mult_zero_l.
 Defined.
 

diff --git a/theories/Algebra/Rings/Vector.v b/theories/Algebra/Rings/Vector.v
@@ -62,9 +62,10 @@ Proof.
 Defined.
 
 Definition path_entry_vector {A : Type} {n : nat} (v : Vector A n)
-  (i : nat) (Hi Hi' : (i < n)%nat)
-  : @entry _ _ v i Hi = @entry _ _ v i Hi'.
+  (i j : nat) (Hi : (i < n)%nat) (Hj : (j < n)%nat) (p : i = j)
+  : entry v i = entry v j.
 Proof.
+  destruct p.
   apply nth'_nth'.
 Defined.