single_mul_single_same — Mathlib

English

Let i ∈ l, j ∈ m, k ∈ n and d ∈ α. Then the product of two elementary matrices satisfies (single i j c) · (single j k d) = single i k (c d).

Русский

Пусть i ∈ l, j ∈ m, k ∈ n и d ∈ α. Тогда произведение двух элементарных матриц дает (single i j c) · (single j k d) = single i k (c d).

LaTeX

$$$$(\\mathrm{single}_{i j} c) * (\\mathrm{single}_{j k} d) = \\mathrm{single}_{i k} (c d).$$$$

Lean4

@[simp]
theorem single_mul_single_same (i : l) (j : m) (k : n) (d : α) : single i j c * single j k d = single i k (c * d) :=
  by
  ext a b
  simp only [mul_apply, single]
  by_cases h₁ : i = a <;> by_cases h₂ : k = b <;> simp [h₁, h₂]

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