kroneckerMap — Mathlib

English

If A and B are diagonal, then their Kronecker product A ⊗ B is diagonal.

Русский

Если A и B диагональны, то их произведение Кронекера A ⊗ B диагонально.

LaTeX

$$$\\forall {\\alpha} {A : Matrix m m \\alpha} {B : Matrix n n \\alpha}, A.IsDiag \\to B.IsDiag \\to (A \\u2297 B).IsDiag$$$

Lean4

/-- Produce a matrix with `f` applied to every pair of elements from `A` and `B`. -/
def kroneckerMap (f : α → β → γ) (A : Matrix l m α) (B : Matrix n p β) : Matrix (l × n) (m × p) γ :=
  of fun (i : l × n) (j : m × p) =>
    f (A i.1 j.1)
      (B i.2 j.2)
        -- TODO: set as an equation lemma for `kroneckerMap`, see https://github.com/leanprover-community/mathlib4/pull/3024

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