Orthogonal #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file contains definitions and properties concerning orthogonality of rows and columns.
Main results #
matrix.has_orthogonal_rows:A.has_orthogonal_rowsmeansAhas orthogonal (with respect todot_product) rows.matrix.has_orthogonal_cols:A.has_orthogonal_colsmeansAhas orthogonal (with respect todot_product) columns.
Tags #
orthogonal
def
matrix.has_orthogonal_rows
{α : Type u_1}
{n : Type u_2}
{m : Type u_3}
[has_mul α]
[add_comm_monoid α]
(A : matrix m n α)
[fintype n] :
Prop
A.has_orthogonal_rows means matrix A has orthogonal rows (with respect to
matrix.dot_product).
Equations
- A.has_orthogonal_rows = ∀ ⦃i₁ i₂ : m⦄, i₁ ≠ i₂ → matrix.dot_product (A i₁) (A i₂) = 0
def
matrix.has_orthogonal_cols
{α : Type u_1}
{n : Type u_2}
{m : Type u_3}
[has_mul α]
[add_comm_monoid α]
(A : matrix m n α)
[fintype m] :
Prop
A.has_orthogonal_rows means matrix A has orthogonal columns (with respect to
matrix.dot_product).
Equations
@[simp]
theorem
matrix.transpose_has_orthogonal_rows_iff_has_orthogonal_cols
{α : Type u_1}
{n : Type u_2}
{m : Type u_3}
[has_mul α]
[add_comm_monoid α]
(A : matrix m n α)
[fintype m] :
Aᵀ has orthogonal rows iff A has orthogonal columns.
@[simp]
theorem
matrix.transpose_has_orthogonal_cols_iff_has_orthogonal_rows
{α : Type u_1}
{n : Type u_2}
{m : Type u_3}
[has_mul α]
[add_comm_monoid α]
(A : matrix m n α)
[fintype n] :
Aᵀ has orthogonal columns iff A has orthogonal rows.
theorem
matrix.has_orthogonal_rows.has_orthogonal_cols
{α : Type u_1}
{n : Type u_2}
{m : Type u_3}
[has_mul α]
[add_comm_monoid α]
{A : matrix m n α}
[fintype m]
(h : A.transpose.has_orthogonal_rows) :
theorem
matrix.has_orthogonal_cols.transpose_has_orthogonal_rows
{α : Type u_1}
{n : Type u_2}
{m : Type u_3}
[has_mul α]
[add_comm_monoid α]
{A : matrix m n α}
[fintype m]
(h : A.has_orthogonal_cols) :
theorem
matrix.has_orthogonal_cols.has_orthogonal_rows
{α : Type u_1}
{n : Type u_2}
{m : Type u_3}
[has_mul α]
[add_comm_monoid α]
{A : matrix m n α}
[fintype n]
(h : A.transpose.has_orthogonal_cols) :
theorem
matrix.has_orthogonal_rows.transpose_has_orthogonal_cols
{α : Type u_1}
{n : Type u_2}
{m : Type u_3}
[has_mul α]
[add_comm_monoid α]
{A : matrix m n α}
[fintype n]
(h : A.has_orthogonal_rows) :