single_mul_single_of_ne — Mathlib

English

Let i ∈ l, j k ∈ m and h : j ≠ k. Then for any d ∈ α, (single i j c) · (single k l d) = 0. In other words, the product of two elementary matrices with incompatible column indices is zero.

Русский

Пусть i ∈ l, j, k ∈ m, и h : j ≠ k. Тогда для любого d ∈ α произведение (single i j c) · (single k l d) равно 0.

LaTeX

$$$$(\\mathrm{single}_{i j} c) · (\\mathrm{single}_{k l} d) = 0 \\quad \\text{если } j \\neq k.$$$$

Lean4

@[simp]
theorem single_mul_single_of_ne (i : l) (j k : m) {l : n} (h : j ≠ k) (d : α) : single i j c * single k l d = 0 :=
  by
  ext a b
  simp only [mul_apply, single, of_apply]
  by_cases h₁ : i = a
  · simp [h₁, h, Finset.sum_eq_zero]
  · simp [h₁]

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