English
For a bijection f: l ≃. m with finite m, the (i,j)-entry of f.toMatrix * M equals the entry from the sum over preimages of j under f.
Русский
Для биекции f: l ≃. m, элемент (i,j) в f.toMatrix * M равен сумме по предобразам j через f.
LaTeX
$$$\\text{Let } f: l \\to m \\text{ bijection}, \\; M \\in M_{m\\times n}(α).\\quad (f.toMatrix * M)_{i j} = \\sum_{f(i)=j} M_{i j}.$$$
Lean4
theorem toMatrix_mul_apply [Fintype m] [DecidableEq m] [NonAssocSemiring α] (f : l ≃. m) (i j) (M : Matrix m n α) :
(f.toMatrix * M :) i j = Option.casesOn (f i) 0 fun fi => M fi j :=
by
dsimp [toMatrix, Matrix.mul_apply]
rcases h : f i with - | fi
· simp
· rw [Finset.sum_eq_single fi] <;> simp +contextual [eq_comm]
