single_eq_single_vecMulVec_single

English

The matrix unit with entry at (i, j) equals the outer product of the i-th row basis vector and the j-th column basis vector, i.e., single i j 1 = vecMulVec (Pi.single i 1) (Pi.single j 1).

Русский

Единичный элемент матрицы в позиции (i, j) равен внешнему произведению i-й строковой единицы и j-й столбцовой единицы: single i j 1 = vecMulVec (Pi.single i 1) (Pi.single j 1).

LaTeX

$$$ \mathrm{single}_{i j} 1 = \mathrm{vecMulVec} (\Pi.{\mathrm{single}} i 1) (\Pi.{\mathrm{single}} j 1) $$$

Lean4

theorem single_eq_single_vecMulVec_single [MulZeroOneClass α] (i : m) (j : n) :
    single i j (1 : α) = vecMulVec (Pi.single i 1) (Pi.single j 1) := by
  simp [-mul_ite, single, vecMulVec, ite_and, Pi.single_apply, eq_comm]

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