mathlib documentation

linear_algebra.matrix.orthogonal

Orthogonal #

This file contains definitions and properties concerning orthogonality of rows and columns.

Main results #

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
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.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.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) :