kronecker — Mathlib

English

The block matrix (A 0; 0 D) is diagonal if A and D are diagonal.

Русский

Блочная матрица (A 0; 0 D) диагональна при диагональности A и D.

LaTeX

$$$\\forall {\\alpha} {A : Matrix m m \\alpha} {D : Matrix n n \\alpha} [Zero \\alpha] (ha : A.IsDiag) (hd : D.IsDiag) : (A.fromBlocks 0 0 D).IsDiag$$$

Lean4

/-- `(A ⊗ B).IsDiag` if both `A` and `B` are diagonal. -/
theorem kronecker [MulZeroClass α] {A : Matrix m m α} {B : Matrix n n α} (hA : A.IsDiag) (hB : B.IsDiag) :
    (A ⊗ₖ B).IsDiag := by
  rintro ⟨a, b⟩ ⟨c, d⟩ h
  simp only [Prod.mk_inj, Ne, not_and_or] at h
  rcases h with hac | hbd
  · simp [hA hac]
  · simp [hB hbd]

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