Orthogonal

📁 Source: Mathlib/LinearAlgebra/Matrix/Orthogonal.lean

Statistics

Metric	Count
Definitions HasOrthogonalCols, HasOrthogonalRows	2
Theorems hasOrthogonalRows, transpose_hasOrthogonalRows, hasOrthogonalCols, transpose_hasOrthogonalCols, transpose_hasOrthogonalCols_iff_hasOrthogonalRows, transpose_hasOrthogonalRows_iff_hasOrthogonalCols	6
Total	8

Matrix

Definitions

Name	Category	Theorems
HasOrthogonalCols 📖	MathDef	5 math math: HasOrthogonalRows.hasOrthogonalCols, transpose_hasOrthogonalCols_iff_hasOrthogonalRows, HasOrthogonalRows.transpose_hasOrthogonalCols, transpose_hasOrthogonalRows_iff_hasOrthogonalCols, transpose_mul_self_isDiag_iff_hasOrthogonalCols
HasOrthogonalRows 📖	MathDef	5 math math: mul_transpose_self_isDiag_iff_hasOrthogonalRows, transpose_hasOrthogonalCols_iff_hasOrthogonalRows, transpose_hasOrthogonalRows_iff_hasOrthogonalCols, HasOrthogonalCols.transpose_hasOrthogonalRows, HasOrthogonalCols.hasOrthogonalRows

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
transpose_hasOrthogonalCols_iff_hasOrthogonalRows 📖	mathematical	—	HasOrthogonalCols transpose HasOrthogonalRows	—	—
transpose_hasOrthogonalRows_iff_hasOrthogonalCols 📖	mathematical	—	HasOrthogonalRows transpose HasOrthogonalCols	—	—

Matrix.HasOrthogonalCols

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasOrthogonalRows 📖	mathematical	Matrix.HasOrthogonalCols Matrix.transpose	Matrix.HasOrthogonalRows	—	—
transpose_hasOrthogonalRows 📖	mathematical	Matrix.HasOrthogonalCols	Matrix.HasOrthogonalRows Matrix.transpose	—	—

Matrix.HasOrthogonalRows

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasOrthogonalCols 📖	mathematical	Matrix.HasOrthogonalRows Matrix.transpose	Matrix.HasOrthogonalCols	—	—
transpose_hasOrthogonalCols 📖	mathematical	Matrix.HasOrthogonalRows	Matrix.HasOrthogonalCols Matrix.transpose	—	—

---

← Back to Index