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,675 to 1,680 of 2,569 results.
Matrix.opNorm_mul_le
Mathematical statement
The operator norm of a matrix product is at most the product of the operator norms.
Source project: quantumInfo
Person-level attribution pending.
Matrix.schur_triangulation
Mathematical 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.
MatrixMap.choi_id_is_PSD
Project documentation
The Choi matrix of a map in symmetric Kraus form is a sum of rank-1 projectors. -/ theorem choi_of_kraus_R [DecidableEq A] (K : κ → Matrix B A 𝕜) : (of_kraus K K).choi_matrix = ∑ k, Matrix.vecMulVec (fun (x : B × A) => K k x.1 x.2) (fun (x : B × A) => star (K k x.1 x.2)) := by unfold of_kraus choi_matrix ext i j : 2 simp only [LinearMap.coe_sum, LinearMa...
Source project: quantumInfo
Person-level attribution pending.
MatrixMap.choi_map_inv
Mathematical statement
Proves that MatrixMap.choi_matrix and MatrixMap.of_choi_matrix inverses.
Source project: quantumInfo
Person-level attribution pending.
MatrixMap.choi_matrix_eq_map_proj
Project documentation
The linear map of conjugating a matrix by another, x → y * x * yᴴ. -/ @[simps] def root.MatrixMap.conj (y : Matrix B A R) : MatrixMap A B R where toFun x := y * x * y.conjTranspose map_add' x y := by rw [Matrix.mul_add, Matrix.add_mul] map_smul' r x := by rw [RingHom.id_apply, Matrix.mul_smul, Matrix.smul_mul] omit [DecidableEq A] in theorem conj_isPo...
Source project: quantumInfo
Person-level attribution pending.
MatrixMap.choi_of_kraus_R
Mathematical statement
The Choi matrix of a map in symmetric Kraus form is a sum of rank-1 projectors.
Source project: quantumInfo
Person-level attribution pending.