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
- Matrix.HasOrthogonalRows A = ∀ ⦃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
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ᵀ 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ᵀ 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 : Matrix.HasOrthogonalRows (Matrix.transpose A))
:
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 : Matrix.HasOrthogonalCols A)
:
theorem
Matrix.HasOrthogonalCols.hasOrthogonalRows
{α : Type u_1}
{n : Type u_2}
{m : Type u_3}
[Mul α]
[AddCommMonoid α]
{A : Matrix m n α}
[Fintype n]
(h : Matrix.HasOrthogonalCols (Matrix.transpose A))
:
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 : Matrix.HasOrthogonalRows A)
: