Orthogonal #
This file contains definitions and properties concerning orthogonality of rows and columns.
Main results #
matrix.HasOrthogonalRows:A.HasOrthogonalRowsmeansAhas orthogonal (with respect todotProduct) rows.matrix.HasOrthogonalCols:A.HasOrthogonalColsmeansAhas orthogonal (with respect todotProduct) 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]
:
A.HasOrthogonalRows means matrix A has orthogonal rows (with respect to
Matrix.dotProduct).
Equations
- A.HasOrthogonalRows = ∀ ⦃i₁ i₂ : m⦄, i₁ ≠ i₂ → Matrix.dotProduct (A i₁) (A i₂) = 0
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
- A.HasOrthogonalCols = A.transpose.HasOrthogonalRows
Instances For
@[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