single_mul_apply_of_ne — Mathlib

English

Let i ∈ l, j ∈ m, a ∈ l, b ∈ n, c ∈ α and M ∈ Matrix m n α. If a ≠ i, then the entry (a,b) of the product (single i j c) · M is zero; i.e., (single i j c · M)_{a b} = 0.

Русский

Пусть i ∈ l, j ∈ m, a ∈ l, b ∈ n, c ∈ α и M ∈ MATRIX(m,n,α). Если a ≠ i, то элемент в позиции (a,b) произведения (единичный) · M равен нулю: (single i j c · M)_{a b} = 0.

LaTeX

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

Lean4

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

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