adapt to mc#1256

math-comp · Nov 4, 2024 · 68d122d · 68d122d
1 parent 21062a5
commit 68d122d
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/theories/complex.v b/theories/complex.v
@@ -1069,6 +1069,7 @@ have [] := @Lemma4 _ _ 1%:M _ [::L1; L2] (erefl _).
   rewrite 4!mul_rV_lin !mxvecK /= /L1fun /L2fun /=; congr (mxvec (_ *: _)).
   move=> {L1 L2 L1fun L2fun}.
   case: n {x} (vec_mx x) => [//|n] x in HrV u v *.
+  rewrite !GRing.sub_funE.
   do ?[rewrite -(scalemxAl, scalemxAr, scalerN, scalerDr)
       |rewrite (mulmxN, mulNmx, trmxK, trmx_mul)
       |rewrite ?[(_ *: _)^T]linearZ ?[(_ + _)^T]linearD ?[(- _)^T]linearN /=].