diag_replicateCol_mul_replicateRow

English

For Mul α and AddCommMonoid α and Unique ι, diag (replicateCol ι a * replicateRow ι b) = a * b, where a,b: n → α.

Русский

При Mul α, AddCommMonoid α и Unique ι диагональ diag (replicateCol ι a * replicateRow ι b) равна точечной произведению a * b.

LaTeX

$$$ \mathrm{diag}(\mathrm{replicateCol}\ ι\ a * \mathrm{replicateRow}\ ι\ b) = a * b $$$

Lean4

@[simp]
theorem diag_replicateCol_mul_replicateRow [Mul α] [AddCommMonoid α] [Unique ι] (a b : n → α) :
    diag (replicateCol ι a * replicateRow ι b) = a * b := by
  ext
  simp [Matrix.mul_apply, replicateCol, replicateRow]

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