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.HasDenseDomain.orthogonal_range
Plain-language statement
U.rangeᗮ = U†.ker c.f. LinearMap.orthogonal_range and ContinuousLinearMap.orthogonal_range
Source project: Physlib
Person-level attribution pending.
LinearPMap.inner_centered_commutator_of_raw_commutator
Plain-language statement
A raw commutator expectation determines the centered commutator expectation.
Source project: Physlib
Person-level attribution pending.
LinearPMap.inner_map_polarization
Plain-language statement
The analogue of inner_map_polarization for LinearPMap.
Source project: Physlib
Person-level attribution pending.
LinearPMap.inner_map_polarization'
Plain-language statement
The analogue of inner_map_polarization' for LinearPMap.
Source project: Physlib
Person-level attribution pending.
LinearPMap.isClosable_of_continuous
Plain-language statement
Continuous operators are closable.
Source project: Physlib
Person-level attribution pending.
LinearPMap.isClosable_of_exists_dense_formalAdjoint
Plain-language statement
A LinearPMap with densely-defined formal adjoint is closable.
Source project: Physlib
Person-level attribution pending.