# Documentation

Mathlib.LinearAlgebra.Matrix.Orthogonal

# 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).

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).

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ᵀ 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ᵀ 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 : ) :
theorem Matrix.HasOrthogonalCols.transpose_hasOrthogonalRows {α : Type u_1} {n : Type u_2} {m : Type u_3} [Mul α] [] {A : Matrix m n α} [] (h : ) :
theorem Matrix.HasOrthogonalCols.hasOrthogonalRows {α : Type u_1} {n : Type u_2} {m : Type u_3} [Mul α] [] {A : Matrix m n α} [] (h : ) :
theorem Matrix.HasOrthogonalRows.transpose_hasOrthogonalCols {α : Type u_1} {n : Type u_2} {m : Type u_3} [Mul α] [] {A : Matrix m n α} [] (h : ) :