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,741 to 1,746 of 2,569 results.
mixed_convex_roof_of_pure
Mathematical statement
The mixed convex roof extension of f : MState d → ℝ≥0 applied to a pure state ψ is f (pure ψ).
Source project: quantumInfo
Person-level attribution pending.
modular_form_tendsto_atImInfty
Mathematical statement
A modular form tends to its value at infinity as z → i∞.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
MSSMACC.AnomalyFreePerp.inQuadSolProp_iff_proj_inQuadProp
Mathematical statement
The conditions inQuadSolProp R and inQuadProp (proj R.1.1) are equivalent. This is to be expected since both R and proj R.1.1 define the same plane with Y₃ and B₃.
Source project: Physlib
Person-level attribution pending.
MSSMACCs.accCube_ext
Project documentation
Extensionality lemma for accCube.
Source project: Physlib
Person-level attribution pending.
MState.fidelity_self_eq_one
Mathematical statement
A state has perfect fidelity with itself.
Source project: quantumInfo
Person-level attribution pending.
MState.Ket.IsProd_iff_rank_eq_one
Mathematical statement
A ket on a product space is a product state if and only if its coefficient matrix has rank 1.
Source project: quantumInfo
Person-level attribution pending.