Theorems · Definition · linear algebra

Matrix.HasOrthogonalRows

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

A.HasOrthogonalRows means matrix A has orthogonal rows (with respect to dotProduct).

Defined in

Mathlib.LinearAlgebra.Matrix.Orthogonal

Cited by

7 results in Mathlib

Foundations

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

Assumes

MulAddCommMonoidFintype