SchurTriangulation

📁 Source: PhysLean/Mathematics/SchurTriangulation.lean

Statistics

Metric	Count
Definitions finAddEquivSigmaCond, sumEquivSigmalCond, subNat', SchurTriangulationAux, basis, dim, of, IsUpperTriangular, UpperTriangular, schurTriangulation, schurTriangulationBasis, schurTriangulationUnitary, instDecidableEqSigmaBoolCond_physLean, instFintypeCond_physLean	14
Theorems finAddEquivSigmaCond_false, finAddEquivSigmaCond_true, hdim, upperTriangular, schur_triangulation	5
Total	19

Equiv

Definitions

Name	Category	Theorems
finAddEquivSigmaCond 📖	CompOp	2 math math: finAddEquivSigmaCond_false, finAddEquivSigmaCond_true
sumEquivSigmalCond 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finAddEquivSigmaCond_false 📖	mathematical	—	finAddEquivSigmaCond Fin.subNat'	—	—
finAddEquivSigmaCond_true 📖	mathematical	—	finAddEquivSigmaCond	—	—

Fin

Definitions

Name	Category	Theorems
subNat' 📖	CompOp	1 math math: Equiv.finAddEquivSigmaCond_false

LinearMap

Definitions

Name	Category	Theorems
SchurTriangulationAux 📖	CompData	—

LinearMap.SchurTriangulationAux

Definitions

Name	Category	Theorems
basis 📖	CompOp	1 math math: upperTriangular
dim 📖	CompOp	2 math math: hdim, upperTriangular
of 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hdim 📖	mathematical	—	dim	—	—
upperTriangular 📖	mathematical	—	Matrix.IsUpperTriangular dim basis	—	—

Matrix

Definitions

Name	Category	Theorems
IsUpperTriangular 📖	MathDef	2 math math: LinearMap.SchurTriangulationAux.upperTriangular, schur_triangulation
UpperTriangular 📖	CompOp	—
schurTriangulation 📖	CompOp	1 math math: schur_triangulation
schurTriangulationBasis 📖	CompOp	—
schurTriangulationUnitary 📖	CompOp	1 math math: schur_triangulation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
schur_triangulation 📖	mathematical	—	schurTriangulationUnitary IsUpperTriangular schurTriangulation	—	—

(root)

Definitions

Name	Category	Theorems
instDecidableEqSigmaBoolCond_physLean 📖	CompOp	—
instFintypeCond_physLean 📖	CompOp	—

---

← Back to Index