transpose_hasOrthogonalRows

Mathlib.LinearAlgebra.Matrix.Orthogonal

URI: https://scilib.ai/kg/mathlib#Matrix.HasOrthogonalCols.transpose_hasOrthogonalRows

English

The dashed dot product of 2-element vectors is a0*b0 + a1*b1.

Русский

Усечённое скалярное произведение векторов длины 2 равно a0*b0 + a1*b1.

LaTeX

$$$v \cdot' w = v_0 w_0 + v_1 w_1$$$

Lean4

theorem transpose_hasOrthogonalRows [Fintype m] (h : A.HasOrthogonalCols) : Aᵀ.HasOrthogonalRows :=
  h

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

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

Разделы

Аффилиация

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