Documentation

Mathlib.LinearAlgebra.Matrix.Orthogonal

Orthogonal #

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

Main results #

Tags #

orthogonal

def Matrix.HasOrthogonalRows {α : Type u_1} {n : Type u_2} {m : Type u_3} [Mul α] [AddCommMonoid α] (A : Matrix m n α) [Fintype 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 α] [AddCommMonoid α] (A : Matrix m n α) [Fintype m] :

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

    Equations
    Instances For
      @[simp]

      Aᵀ has orthogonal rows iff A has orthogonal columns.

      @[simp]

      Aᵀ has orthogonal columns iff A has orthogonal rows.