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
  • A.HasOrthogonalRows = ∀ ⦃i₁ i₂ : m⦄, i₁ ≠ i₂ → A i₁ ⬝ᵥ A i₂ = 0
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
    • A.HasOrthogonalCols = A.transpose.HasOrthogonalRows
    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