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,573 to 1,578 of 2,569 results.
LinearPMap.resolventSet_eq_empty
Mathematical statement
If an operator is not closed then its resolvent set is empty.
Source project: Physlib
Person-level attribution pending.
LinearPMap.resolventSet_isOpen
Mathematical statement
The resolvent set is an open subset of ℂ.
Source project: Physlib
Person-level attribution pending.
LinearPMap.standardDeviation_eq_zero_iff_isEigenvector
Mathematical statement
For ‖ψ‖ = 1, zero standard deviation iff the eigenvector condition holds.
Source project: Physlib
Person-level attribution pending.
LinearPMap.state_uncertainty_squared_with_covariance_of_centered_commutator
Mathematical statement
A centered commutator identity implies the Robertson–Schrödinger uncertainty bound.
Source project: Physlib
Person-level attribution pending.
LinearPMap.unitaryConj_isSelfAdjoint
Mathematical 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.
LinearPMap.unitaryConj_sub_smul_surjective
Mathematical statement
If A - z is surjective for a scalar z : ℂ, then so is u A u⁻¹ - z.
Source project: Physlib
Person-level attribution pending.