kronecker_diagonal — Mathlib

English

The Kronecker product of two diagonals is diagonal with entrywise products.

Русский

Кронекерово произведение двух диагональных матриц — диагональная матрица с попарными произведениями элементов.

LaTeX

$$diagonal(a) ⊗ diagonal(b) = diagonal(fun mn => a mn.fst * b mn.snd)$$

Lean4

theorem kronecker_diagonal [MulZeroClass α] [DecidableEq n] (A : Matrix l m α) (b : n → α) :
    A ⊗ₖ diagonal b = blockDiagonal fun i => A <• b i :=
  kroneckerMap_diagonal_right _ mul_zero _ _

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