add

Mathlib.LinearAlgebra.Matrix.IsDiag

URI: https://scilib.ai/kg/mathlib#Matrix.IsDiag.add

English

If A and B are diagonal matrices, then their sum A + B is diagonal.

Русский

Если A и B диагональные, то их сумма A + B диагональна.

LaTeX

$$$\\forall {\\alpha} {n} [AddZeroClass \\alpha] {A B : Matrix n n \\alpha}, A.IsDiag \\to B.IsDiag \\to (A + B).IsDiag$$$

Lean4

theorem add [AddZeroClass α] {A B : Matrix n n α} (ha : A.IsDiag) (hb : B.IsDiag) : (A + B).IsDiag :=
  by
  intro i j h
  simp [ha h, hb h]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru