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 2,569 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.
Showing 1,669 to 1,674 of 2,569 results.
Matrix.det_exp_of_blockTriangular_id
Mathematical statement
Lie's trace formula for upper triangular matrices.
Source project: Physlib
Person-level attribution pending.
Matrix.det_exp_real
Mathematical 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.full_row_rank_via_rank_subLeftFull
Mathematical statement
An m×n matrix has full rank if the submatrix consisting of columns 1 through m has rank m.
Source project: ArkLib
Person-level attribution pending.
Matrix.getM_option_eq_some_iff
Mathematical statement
getM at Option succeeds exactly when every component does. This is what turns the func branch of ofNat into a statement about each argument separately.
Source project: Foundation
Person-level attribution pending.
Matrix.isometry_preserves_norm
Project documentation
The operator norm of a matrix, with respect to the Euclidean norm (l2 norm) on the domain and codomain. -/ noncomputable def Matrix.opNorm [RCLike 𝕜] (A : Matrix m n 𝕜) : ℝ := ‖LinearMap.toContinuousLinearMap (Matrix.toEuclideanLin A)‖ /- An isometry preserves the Euclidean norm.
Source project: quantumInfo
Person-level attribution pending.
Matrix.opNorm_isometry
Project documentation
The operator norm of a matrix, with respect to the Euclidean norm (l2 norm) on the domain and codomain. -/ noncomputable def Matrix.opNorm [RCLike 𝕜] (A : Matrix m n 𝕜) : ℝ := ‖LinearMap.toContinuousLinearMap (Matrix.toEuclideanLin A)‖ /- An isometry preserves the Euclidean norm. -/ theorem Matrix.isometry_preserves_norm (A : Matrix n m 𝕜) (hA : A.Isom...
Source project: quantumInfo
Person-level attribution pending.