single_mul_single_of_ne — Mathlib

English

If E_{a,b1} and E_{b2,c} are elementary matrices with b1 ≠ b2, then their product is the zero matrix: E_{a,b1} E_{b2,c} = 0.

Русский

Если E_{a,b1} и E_{b2,c} — элементарные матрицы, и b1 ≠ b2, то их произведение равно нулевой матрице: E_{a,b1} E_{b2,c} = 0.

LaTeX

$$$b_1 \\neq b_2 \\implies E_{a,b_1} E_{b_2,c} = 0$$$

Lean4

theorem single_mul_single_of_ne [Fintype n] [DecidableEq n] [DecidableEq k] [DecidableEq m] [NonAssocSemiring α]
    {b₁ b₂ : n} (hb : b₁ ≠ b₂) (a : m) (c : k) : (single a b₁).toMatrix * (single b₂ c).toMatrix = (0 : Matrix _ _ α) :=
  by rw [← toMatrix_trans, single_trans_single_of_ne hb, toMatrix_bot]

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