mul_apply_eq_vecMul — Mathlib

English

Let A be an m×n matrix and B be an n×o matrix over a semiring. Then the i-th row of the product AB is obtained by taking the i-th row of A and multiplying it by B on the right.

Русский

Пусть A – матрица размером m×n, B – матрица размером n×o над полем или полугруппа. Тогда i-я строка произведения AB равна i-й строке A, умноженной на B справа.

LaTeX

$$$(AB)_{i,*} = (A_{i,*}) B\quad\text{for all } i.$$$

Lean4

/-- The `i`th row of the multiplication is the same as the `vecMul` with the `i`th row of `A`. -/
theorem mul_apply_eq_vecMul [Fintype n] (A : Matrix m n α) (B : Matrix n o α) (i : m) : (A * B) i = A i ᵥ* B :=
  rfl

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