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 filtersPauliMatrix.pauliSelfAdjoint_span
Plain-language statement
The Pauli matrices span all self-adjoint matrices.
Source project: Physlib
Person-level attribution pending.
PauliMatrix.pauliSelfAdjoint'_linearly_independent
Plain-language statement
The Pauli matrices where σi are negated are linearly independent.
Source project: Physlib
Person-level attribution pending.
PauliMatrix.pauliSelfAdjoint'_span
Plain-language statement
The Pauli matrices where σi are negated span all Self-adjoint matrices.
Source project: Physlib
Person-level attribution pending.
PauliMatrix.selfAdjoint_ext
Plain-language statement
Two 2×2 self-adjoint matrices are equal if the real traces of each matrix multiplied by each of the Pauli-matrices are equal.
Source project: Physlib
Person-level attribution pending.
PauliMatrix.selfAdjoint_ext_complex
Plain-language statement
Two 2×2 self-adjoint matrices are equal if the (complex) traces of each matrix multiplied by each of the Pauli-matrices are equal.
Source project: Physlib
Person-level attribution pending.
Physlib.deriv_gaussian_eq_physHermite_mul_gaussian
Project documentation
The Physicists Hermite polynomial are defined as polynomials over ℤ in X recursively with physHermite 0 = 1 and physHermite (n + 1) = 2 • X * physHermite n - derivative (physHermite n). This polynomial will often be cast as a function ℝ → ℝ by evaluating the polynomial at X. -/ noncomputable def physHermite : ℕ → Polynomial ℤ | 0 => 1 | n + 1...
Source project: Physlib
Person-level attribution pending.