mul_single_apply_of_ne — Mathlib

English

Let i ∈ l, j ∈ m, a ∈ l, b ∈ n, hbj : b ≠ j, c ∈ α and M ∈ Matrix l m α. Then (M · single i j c)_{a b} = 0 for hbj, i.e., the column j of M is annihilated outside j.

Русский

Пусть i ∈ l, j ∈ m, a ∈ l, b ∈ n, hbj: b ≠ j, c ∈ α и M ∈ Matrix(l,m,α). Тогда (M · single i j c)_{a b} = 0 при hbj; колонка j в M зануляется вне позиции j.

LaTeX

$$$\\\\forall (i : m) (j : n) (a : l) (b : n) (hbj : b \\neq j) (M : Matrix l m α), (M * single i j c)_{a b} = 0$$$

Lean4

@[simp]
theorem mul_single_apply_of_ne (i : m) (j : n) (a : l) (b : n) (hbj : b ≠ j) (M : Matrix l m α) :
    (M * single i j c) a b = 0 := by simp [mul_apply, hbj.symm]

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