Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 591 research declarations. Search 10,000 more complete Mathlib declarations.
591 results
Clear filtersMatrix.blockTriangular_exp_of_blockTriangular_id
Plain-language statement
The exponential of an upper-triangular matrix is upper-triangular.
Source project: Physlib
Person-level attribution pending.
Matrix.det_exp
Plain-language statement
The determinant of the exponential of a matrix is the exponential of its trace. This is also known as Lie's trace formula.
Source project: Physlib
Person-level attribution pending.
Matrix.det_exp_of_blockTriangular_id
Plain-language statement
Lie's trace formula for upper triangular matrices.
Source project: Physlib
Person-level attribution pending.
Matrix.det_exp_real
Plain-language statement
Lie's trace formula over ℝ: det(exp(A)) = exp(tr(A)) for any real matrix A. This is proved by transferring the result from ℂ using the naturality of polynomial identities.
Source project: Physlib
Person-level attribution pending.
Matrix.schur_triangulation
Plain-language statement
Schur triangulation, Schur decomposition for matrices over an algebraically closed field. In particular, a complex matrix can be converted to upper-triangular form by a change of basis. In other words, any complex matrix is unitarily similar to an upper triangular matrix.
Source project: Physlib
Person-level attribution pending.
MicroHamiltonian.entropy_A_eq_entropy_Z
Plain-language statement
The two definitions of entropy, in terms of T or β = 1 / T, are equivalent.
Source project: Physlib
Person-level attribution pending.