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 α] [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

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

@[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.

@[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.

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

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

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

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