single_mul_single_right — Mathlib

English

For any matrix M, E_{a,b} (E_{b,c} M) = E_{a,c} M.

Русский

Для любой матрицы M выполняется E_{a,b} (E_{b,c} M) = E_{a,c} M.

LaTeX

$$$E_{a,b} (E_{b,c} M) = E_{a,c} M$$$

Lean4

/-- Restatement of `single_mul_single`, which will simplify expressions in `simp` normal form,
  when associativity may otherwise need to be carefully applied. -/
@[simp]
theorem single_mul_single_right [Fintype n] [Fintype k] [DecidableEq n] [DecidableEq k] [DecidableEq m] [Semiring α]
    (a : m) (b : n) (c : k) (M : Matrix k l α) :
    (single a b).toMatrix * ((single b c).toMatrix * M) = (single a c).toMatrix * M := by
  rw [← Matrix.mul_assoc, single_mul_single]

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