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,549 to 1,554 of 2,569 results.
LinearPMap.inner_centered_commutator_of_raw_commutator
Mathematical statement
A raw commutator expectation determines the centered commutator expectation.
Source project: Physlib
Person-level attribution pending.
LinearPMap.inner_map_polarization
Mathematical statement
The analogue of inner_map_polarization for LinearPMap.
Source project: Physlib
Person-level attribution pending.
LinearPMap.inner_map_polarization'
Mathematical statement
The analogue of inner_map_polarization' for LinearPMap.
Source project: Physlib
Person-level attribution pending.
LinearPMap.isClosable_of_continuous
Mathematical statement
Continuous operators are closable.
Source project: Physlib
Person-level attribution pending.
LinearPMap.isClosable_of_exists_dense_formalAdjoint
Mathematical statement
A LinearPMap with densely-defined formal adjoint is closable.
Source project: Physlib
Person-level attribution pending.
LinearPMap.IsClosable.add_continuous
Mathematical statement
Closability is preserved upon adding a continuous operator.
Source project: Physlib
Person-level attribution pending.