mathlib3 documentation

linear_algebra.matrix.orthogonal

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 #

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]

Aᵀ has orthogonal rows iff A has orthogonal columns.

@[simp]

Aᵀ has orthogonal columns iff A has orthogonal rows.