Documentation

Mathlib.LinearAlgebra.Matrix.Orthogonal

Orthogonal #

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

Main results #

Tags #

orthogonal

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

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

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

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

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

          Aᵀ has orthogonal rows iff A has orthogonal columns.

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

          Aᵀ has orthogonal columns iff A has orthogonal rows.

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