transpose_add

Mathlib.LinearAlgebra.Matrix.Defs

URI: https://scilib.ai/kg/mathlib#Matrix.transpose_add

English

The transpose respects addition: (M+N)ᵀ = Mᵀ + Nᵀ.

Русский

Транспонирование сохраняет сложение: (M+N)ᵀ = Mᵀ + Nᵀ.

LaTeX

$$$ (M + N)^{\\mathrm{T}} = M^{\\mathrm{T}} + N^{\\mathrm{T}} $$$

Lean4

@[simp]
theorem transpose_add [Add α] (M : Matrix m n α) (N : Matrix m n α) : (M + N)ᵀ = Mᵀ + Nᵀ :=
  by
  ext
  simp

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

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

Разделы

Аффилиация

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