English
Let i ∈ l, i' ∈ m, j' ∈ n, j ∈ o, a ∈ α and x ∈ Matrix m n α, b ∈ α. Then (single i i' a) · x · (single j' j b) = single i j (a · x_{i' j'} · b). This describes how a scalar is carried through a sandwich of elementary matrices around a general matrix.
Русский
Пусть i ∈ l, i' ∈ m, j' ∈ n, j ∈ o, a ∈ α и x ∈ Matrix(m,n,α), b ∈ α. Тогда (single i i' a) · x · (single j' j b) = single i j (a · x_{i' j'} · b).
LaTeX
$$$$(\\mathrm{single}_{i i'} a) * x * (\\mathrm{single}_{j' j} b) = \\mathrm{single}_{i j} (a * x_{i' j'} * b).$$$$
Lean4
@[simp]
theorem single_mul_mul_single [Fintype n] (i : l) (i' : m) (j' : n) (j : o) (a : α) (x : Matrix m n α) (b : α) :
single i i' a * x * single j' j b = single i j (a * x i' j' * b) :=
by
ext i'' j''
simp only [mul_apply, single]
by_cases h₁ : i = i'' <;> by_cases h₂ : j = j'' <;> simp [h₁, h₂]
