LieTrace

📁 Source: PhysLean/Mathematics/DataStructures/Matrix/LieTrace.lean

Statistics

Metric	Count
Definitions instUniformSpace_physLean	1
Theorems pow, blockTriangular_exp_of_blockTriangular_id, det_exp, det_exp_of_blockTriangular_id, det_exp_real, det_exp_unitary_conj, det_unitary_conj, diag_exp_of_blockTriangular_id, diag_mul_of_blockTriangular_id, diag_pow_entry_eq_pow_diag_entry, diag_pow_of_blockTriangular_id, exp_series_diag_term_eq, exp_unitary_conj, map_tsum, matrix_exp_series_diag_eq_scalar_series, matrix_tsum_apply, trace_unitary_conj, tsum_eq_zero, exp_map_algebraMap	19
Total	20

Matrix

Definitions

Name	Category	Theorems
instUniformSpace_physLean 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
blockTriangular_exp_of_blockTriangular_id 📖	—	—	—	—	matrix_tsum_apply tsum_eq_zero
det_exp 📖	—	—	—	—	schur_triangulation trace_unitary_conj det_exp_unitary_conj det_exp_of_blockTriangular_id
det_exp_of_blockTriangular_id 📖	—	—	—	—	blockTriangular_exp_of_blockTriangular_id diag_exp_of_blockTriangular_id
det_exp_real 📖	—	—	—	—	det_exp NormedSpace.exp_map_algebraMap
det_exp_unitary_conj 📖	—	—	—	—	exp_unitary_conj det_unitary_conj
det_unitary_conj 📖	—	—	—	—	—
diag_exp_of_blockTriangular_id 📖	—	—	—	—	matrix_tsum_apply matrix_exp_series_diag_eq_scalar_series
diag_mul_of_blockTriangular_id 📖	—	—	—	—	—
diag_pow_entry_eq_pow_diag_entry 📖	—	—	—	—	diag_pow_of_blockTriangular_id
diag_pow_of_blockTriangular_id 📖	—	—	—	—	blockTriangular.pow diag_mul_of_blockTriangular_id
exp_series_diag_term_eq 📖	—	—	—	—	diag_pow_entry_eq_pow_diag_entry
exp_unitary_conj 📖	—	—	—	—	—
map_tsum 📖	—	—	—	—	—
matrix_exp_series_diag_eq_scalar_series 📖	—	—	—	—	exp_series_diag_term_eq
matrix_tsum_apply 📖	—	—	—	—	—
trace_unitary_conj 📖	—	—	—	—	—
tsum_eq_zero 📖	—	—	—	—	—

Matrix.blockTriangular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pow 📖	—	—	—	—	—

NormedSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exp_map_algebraMap 📖	—	—	—	—	Matrix.map_tsum

---

← Back to Index