I had been trying this small proof with mathcomp matrix:

```
Goal
let mt: 'M[bool]_(2,3) := \matrix_(i<2, j<3) (if i == 0 && (j == 1) :> nat then 1 else 0) in
let rw := (\row_i (if i == 0 then 1 else 0)) *m mt in
(\sum_j (rw 0 j)) == 1.
Proof.
```

But I couldn't make any progress on solving it.

Because on doing a simplification, the goal became

```
\sum_(j < 3)
(\row_i (if i == 0 then 1 else 0) *m \matrix_(i, _)
(if i == 0%N then 1 else 0)) 0 j == 1
```

Can we simplify using definition of `*m`

here? `rewrite mxE`

didn't work. Possibly because the `*m`

is inside the `\sum`

?

Apparently, we don't even need to unfold the matrix multiplication explicitly, this works:

```
From mathcomp Require Import all_ssreflect all_algebra.
Local Open Scope ring_scope.
Goal
let mt: 'M[bool]_(2,3) := \matrix_(i<2, j<3) (if i == 0 && (j == 1) :> nat then 1 else 0) in
let rw := (\row_i (if i == 0 then 1 else 0)) *m mt in
(\sum_j (rw 0 j)) == 1.
Proof. by do 2 ![rewrite /= !big_ord_recl !big_ord0 !mxE]. Qed.
```

Possibly because the *m is inside the \sum?

Yeah plain `rewrite`

(vanilla or ssreflect) typically does not work under binders (and `\sum_j`

binds `j`

), but there are alternatives (for ssreflect that's `under`

)

Last updated: Jul 23 2024 at 20:01 UTC