mul_val_succ — Mathlib

English

For A with a tail, the (i.succ, j) entry of A B equals the corresponding product with the tail of A.

Русский

Для матрицы A с хвостом, элемент (i.succ, j) произведения A B равен соответствующему произведению с хвостом A.

LaTeX

$$$\\text{(A * B)}_{i.succ,j} = \\big(\\mathrm{of}(\\mathrm{vecTail}(\\mathrm{of.symm} A)) * B\\big)_{i j}$$$

Lean4

theorem mul_val_succ [Fintype n'] (A : Matrix (Fin m.succ) n' α) (B : Matrix n' o' α) (i : Fin m) (j : o') :
    (A * B) i.succ j = (of (vecTail (of.symm A)) * B) i j :=
  rfl

Похожие утверждения