LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

$E_{i j} E_{k ℓ} = δ_{j k} E_{i ℓ}$

Statement

For $E_{i j} \in M_{m \times n} (F)$ and $E_{k ℓ} \in M_{n \times p} (F)$ ,

$E_{i j} E_{k ℓ} = δ_{j k} E_{i ℓ} .$

Facts & Assumptions

Given: A field $F$ and indices $i < m$ , $j, k < n$ , and $ℓ < p$ .

[L1]

The matrix unit $E_{i j}$ has entry $δ_{r i} δ_{s j}$ in position $(r, s)$ (Matrix units $E_{i j}$ and the Kronecker delta).

Proof

technique · direct

1.1

For $r < m$ and $s < p$ , the product entry is $(E_{i j} E_{k ℓ})_{r s} = \sum_{t < n} δ_{r i} δ_{t j} δ_{t k} δ_{s ℓ}$ .

givenL1

2.1

If $j \neq k$ , every summand is zero. If $j = k$ , only $t = j$ can contribute and the value is $δ_{r i} δ_{s ℓ}$ .

step 1.1L1

3.1

The two cases combine as $(E_{i j} E_{k ℓ})_{r s} = δ_{j k} (E_{i ℓ})_{r s}$ for every entry, proving the matrix identity.

step 2.1L1∎

Depends on

Used by

Mₙ(F) is noncommutative for every n≥2 Corollary
A nonzero square-zero matrix is not similar to any diagonal matrix Example
Two explicit 2 by 2 matrices do not commute Example

Dependency tree · two levels

4 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

P. E. Leonard, Linear Algebra Notes, §3.4 (standard reference, not scraped)

EijEkℓ=δjkEiℓEij​Ekℓ​=δjk​Eiℓ​