single_hadamard_single_eq — Mathlib

English

Let E_{ij}(a) denote the matrix with a in the (i,j) position and zeros elsewhere. Then for all i ∈ m, j ∈ n and a,b ∈ α, E_{ij}(a) ⊙ E_{ij}(b) = E_{ij}(a b).

Русский

Пусть E_{ij}(a) обозначает матрицу, в которой на позиции (i, j) стоит a, а все остальные элементы равны нулю. Тогда для любых i ∈ m, j ∈ n и a,b ∈ α выполняется E_{ij}(a) ⊙ E_{ij}(b) = E_{ij}(a b).

LaTeX

$$$E_{ij}(a) \odot E_{ij}(b) = E_{ij}(a b)$$$

Lean4

theorem single_hadamard_single_eq (i : m) (j : n) (a b : α) : single i j a ⊙ single i j b = single i j (a * b) :=
  ext fun _ _ => (apply_ite₂ _ _ _ _ _ _).trans (congr_arg _ <| zero_mul 0)

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