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 filtersLinearPMap.IsFormalAdjoint.unitaryConj
Plain-language statement
Unitary conjugation preserves formal adjointness. If A is a formal adjoint of B, then u A u⁻¹ is a formal adjoint of u B u⁻¹. Unitary conjugation preserves symmetry when A = B.
Source project: Physlib
Person-level attribution pending.
LinearPMap.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.IsSymmetric.closure
Plain-language statement
The closure of a symmetric densely-defined operator is symmetric: T†† is a symmetric closed extension of T, so it extends T.closure, whose symmetry then descends.
Source project: Physlib
Person-level attribution pending.
LinearPMap.IsSymmetric.Iio_subset_regularityDomain
Plain-language statement
If m is a lower bound on the numerical range then the regularity domain contains (-∞,m).
Source project: Physlib
Person-level attribution pending.
LinearPMap.IsSymmetric.isEssentiallySelfAdjoint_of_defectNumber_eq_zero
Plain-language statement
The basic criterion for essential self-adjointness: a symmetric, densely-defined operator whose defect numbers at I and -I both vanish is essentially self-adjoint.
Source project: Physlib
Person-level attribution pending.
LinearPMap.IsSymmetric.isSelfAdjoint_of_range_eq_top
Plain-language statement
Self-adjointness from surjectivity of T ± i: a symmetric, densely-defined operator T for which T + I • 1 and T - I • 1 both have full range is self-adjoint.
Source project: Physlib
Person-level attribution pending.