English
If A is the matrix vecCons v A, then the product with B equals a matrix whose first row is vecMul v B and whose remaining rows come from AB, assembled via the reverse embedding.
Русский
Если матрица A составляет vecCons v A, то произведение A B равно матрице, где первая строка — vecMul v B, а оставшиеся строки получаются из AB и собираются обратно.
LaTeX
$$$\\mathrm{of}(\\vecCons v A) * B = \\mathrm{of}(\\vecCons (\\mathrm{vecMul}\, v\, B) (\\mathrm{of.symm}(\\mathrm{of} A * B)))$$$
Lean4
@[simp]
theorem cons_mul [Fintype n'] (v : n' → α) (A : Fin m → n' → α) (B : Matrix n' o' α) :
of (vecCons v A) * B = of (vecCons (v ᵥ* B) (of.symm (of A * B))) :=
by
ext i j
refine Fin.cases ?_ ?_ i
· rfl
simp [mul_val_succ]
