mul_apply' — Mathlib

English

The dot product distributes over the subtraction in the second argument: u ⬝ᵥ (v - w) = u ⬝ᵥ v - u ⬝ᵥ w.

Русский

Скалярное произведение распределяется по вычитанию во втором аргументе: u ⬝ᵥ (v - w) = u ⬝ᵥ v - u ⬝ᵥ w.

LaTeX

$$$ u \cdot (v - w) = u \cdot v - u \cdot w $$$

Lean4

theorem mul_apply' [Fintype m] [Mul α] [AddCommMonoid α] {M : Matrix l m α} {N : Matrix m n α} {i k} :
    (M * N) i k = (M i) ⬝ᵥ fun j => N j k :=
  rfl

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