HasOrthogonalRows

Mathlib.LinearAlgebra.Matrix.Orthogonal

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

← MathLib Explorer

English

The dot product of two 3-element vectors equals a0 b0 + a1 b1 + a2 b2.

Русский

Скалярное произведение двух векторов длины 3 равно a0 b0 + a1 b1 + a2 b2.

LaTeX

$$$v \cdot w = v_0 w_0 + v_1 w_1 + v_2 w_2$$$

Lean4

/-- `A.HasOrthogonalRows` means matrix `A` has orthogonal rows (with respect to
`dotProduct`). -/
def HasOrthogonalRows [Fintype n] : Prop :=
  ∀ ⦃i₁ i₂⦄, i₁ ≠ i₂ → A i₁ ⬝ᵥ A i₂ = 0

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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