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 filtersKroneckerDelta.generalizedKroneckerDelta_swap
Plain-language statement
Swapping two of the upper indices of the generalized Kronecker delta negates it. This is one row transposition of the underlying determinant.
Source project: Physlib
Person-level attribution pending.
LinearPMap.ball_subset_regularityDomain
Plain-language statement
The regularity domain of T contains open balls with radii controlled by the lower bounds.
Source project: Physlib
Person-level attribution pending.
LinearPMap.closure_domain_eq_domain_closure_of_continuous
Plain-language statement
A strengthening of closure_domain_le_domain_closure for continuous operators.
Source project: Physlib
Person-level attribution pending.
LinearPMap.compl_closure_numericalRange_subset_regularityDomain
Plain-language statement
The regularity domain contains the exterior of the numerical range.
Source project: Physlib
Person-level attribution pending.
LinearPMap.covariance_comm
Plain-language statement
Swapping the two observables does not change the covariance.
Source project: Physlib
Person-level attribution pending.
LinearPMap.covariance_eq_re_symm_centered
Plain-language statement
Covariance as the real part of the symmetrized centered inner product.
Source project: Physlib
Person-level attribution pending.