single_mul_single — Mathlib

English

Let E_{a,b} and E_{b,c} denote the matrix units (the matrices with a single 1 in position (a,b) and (b,c) respectively, and zeros elsewhere). Then E_{a,b} E_{b,c} = E_{a,c}.

Русский

Пусть E_{a,b} и E_{b,c} — элементарные матрицы-единицы (единицы в позициях (a,b) и (b,c) соответственно, нули повсюду). Тогда E_{a,b} E_{b,c} = E_{a,c}.

LaTeX

$$$E_{a,b} E_{b,c} = E_{a,c}$$$

Lean4

@[simp]
theorem single_mul_single [Fintype n] [DecidableEq k] [DecidableEq m] [DecidableEq n] [NonAssocSemiring α] (a : m)
    (b : n) (c : k) : ((single a b).toMatrix : Matrix _ _ α) * (single b c).toMatrix = (single a c).toMatrix := by
  rw [← toMatrix_trans, single_trans_single]

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