Theorems · Definition · linear algebra

Matrix.HasOrthogonalCols

{α : Type u_1} → {n : Type u_2} → {m : Type u_3} → [Mul α] → [AddCommMonoid α] → Matrix m n α → [Fintype m] → Prop

A.HasOrthogonalCols means matrix A has orthogonal columns (with respect to dotProduct).

Defined in

Mathlib.LinearAlgebra.Matrix.Orthogonal

Cited by

7 results in Mathlib

Foundations

Depth 16 from the axioms · uses propext, Quot.sound

Assumes

MulAddCommMonoidFintype