single_hadamard_single_of_ne — Mathlib

English

If E_{ij}(a) and E_{kl}(b) are supported at different positions (i,j) ≠ (k,l), then E_{ij}(a) ⊙ E_{kl}(b) = 0.

Русский

Если позиции ненулевых элементов матриц E_{ij}(a) и E_{kl}(b) различны, то их поэлементное произведение равно нулю: E_{ij}(a) ⊙ E_{kl}(b) = 0.

LaTeX

$$$\forall i,j,k,l,a,b,\ (i \neq k \lor j \neq l) \Rightarrow E_{ij}(a) \odot E_{kl}(b) = 0$$$

Lean4

theorem single_hadamard_single_of_ne {ia : m} {ja : n} {ib : m} {jb : n} (h : ¬(ia = ib ∧ ja = jb)) (a b : α) :
    single ia ja a ⊙ single ib jb b = 0 := by
  rw [not_and_or] at h
  cases h <;> (simp only [single]; aesop)

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