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 13 research declarations. Search 10,000 more complete Mathlib declarations.
13 results
Clear filtersLinearPMap.IsSelfAdjoint.mem_resolventSet_of_range_eq_top
Plain-language statement
(T - z • 1).range = ⊤ is a sufficient condition for z ∈ ρ T (and it is a necessary condition by definition of ρ).
Source project: Physlib
Person-level attribution pending.
LinearPMap.unitaryConj_isSelfAdjoint
Plain-language statement
Unitary conjugation preserves self-adjointness: if A is a self-adjoint operator on H and u : H ≃ₗᵢ[ℂ] H' is unitary, then u A u⁻¹ is self-adjoint on H'. Symmetry, dense domain, and the two deficiency surjectivities of A all transfer through u.
Source project: Physlib
Person-level attribution pending.
PauliMatrix.pauliBasis'_decomp
Plain-language statement
The decomposition of a self-adjoint matrix into the Pauli matrices (where σi are negated).
Source project: Physlib
Person-level attribution pending.
PauliMatrix.pauliBasis'_repr_inl_0
Plain-language statement
The component of a self-adjoint matrix in the direction σ0 under the basis formed by the covariant Pauli matrices.
Source project: Physlib
Person-level attribution pending.
PauliMatrix.pauliBasis'_repr_inr_0
Plain-language statement
The component of a self-adjoint matrix in the direction -σ1 under the basis formed by the covariant Pauli matrices.
Source project: Physlib
Person-level attribution pending.
PauliMatrix.pauliBasis'_repr_inr_1
Plain-language statement
The component of a self-adjoint matrix in the direction -σ2 under the basis formed by the covariant Pauli matrices.
Source project: Physlib
Person-level attribution pending.