# Orthogonal #

This file contains definitions and properties concerning orthogonality of rows and columns.

## Main results #

• matrix.HasOrthogonalRows: A.HasOrthogonalRows means A has orthogonal (with respect to dotProduct) rows.
• matrix.HasOrthogonalCols: A.HasOrthogonalCols means A has orthogonal (with respect to dotProduct) columns.

## Tags #

orthogonal

def Matrix.HasOrthogonalRows {α : Type u_1} {n : Type u_2} {m : Type u_3} [Mul α] [] (A : Matrix m n α) [] :

A.HasOrthogonalRows means matrix A has orthogonal rows (with respect to Matrix.dotProduct).

Equations
Instances For
def Matrix.HasOrthogonalCols {α : Type u_1} {n : Type u_2} {m : Type u_3} [Mul α] [] (A : Matrix m n α) [] :

A.HasOrthogonalCols means matrix A has orthogonal columns (with respect to Matrix.dotProduct).

Equations
• A.HasOrthogonalCols = A.transpose.HasOrthogonalRows
Instances For
@[simp]
theorem Matrix.transpose_hasOrthogonalRows_iff_hasOrthogonalCols {α : Type u_1} {n : Type u_2} {m : Type u_3} [Mul α] [] (A : Matrix m n α) [] :
A.transpose.HasOrthogonalRows A.HasOrthogonalCols

Aᵀ has orthogonal rows iff A has orthogonal columns.

@[simp]
theorem Matrix.transpose_hasOrthogonalCols_iff_hasOrthogonalRows {α : Type u_1} {n : Type u_2} {m : Type u_3} [Mul α] [] (A : Matrix m n α) [] :
A.transpose.HasOrthogonalCols A.HasOrthogonalRows

Aᵀ has orthogonal columns iff A has orthogonal rows.

theorem Matrix.HasOrthogonalRows.hasOrthogonalCols {α : Type u_1} {n : Type u_2} {m : Type u_3} [Mul α] [] {A : Matrix m n α} [] (h : A.transpose.HasOrthogonalRows) :
A.HasOrthogonalCols
theorem Matrix.HasOrthogonalCols.transpose_hasOrthogonalRows {α : Type u_1} {n : Type u_2} {m : Type u_3} [Mul α] [] {A : Matrix m n α} [] (h : A.HasOrthogonalCols) :
A.transpose.HasOrthogonalRows
theorem Matrix.HasOrthogonalCols.hasOrthogonalRows {α : Type u_1} {n : Type u_2} {m : Type u_3} [Mul α] [] {A : Matrix m n α} [] (h : A.transpose.HasOrthogonalCols) :
A.HasOrthogonalRows
theorem Matrix.HasOrthogonalRows.transpose_hasOrthogonalCols {α : Type u_1} {n : Type u_2} {m : Type u_3} [Mul α] [] {A : Matrix m n α} [] (h : A.HasOrthogonalRows) :
A.transpose.HasOrthogonalCols