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.unitaryConj_sub_smul_surjective
Plain-language statement
If A - z is surjective for a scalar z : ℂ, then so is u A u⁻¹ - z.
Source project: Physlib
Person-level attribution pending.
LinearPMap.variance_eq_norm_sq_sub_expectedValue_sq
Plain-language statement
For symmetric T and ‖ψ‖ = 1, variance equals ‖Tψ‖ ^ 2 - ⟨T⟩_ψ ^ 2.
Source project: Physlib
Person-level attribution pending.
LinearPMap.variance_eq_zero_iff_isEigenvector
Plain-language statement
For ‖ψ‖ = 1, zero variance iff ψ is an eigenvector with eigenvalue ⟨T⟩_ψ.
Source project: Physlib
Person-level attribution pending.
Lorentz.coContrToMatrix_symm_expand_tmul
Plain-language statement
Expansion of coContrToMatrix in terms of the standard basis.
Source project: Physlib
Person-level attribution pending.
Lorentz.coContrToMatrixRe_symm_expand_tmul
Plain-language statement
Expansion of coContrToMatrixRe in terms of the standard basis.
Source project: Physlib
Person-level attribution pending.
Lorentz.coContrUnitVal_expand_tmul
Plain-language statement
Expansion of coContrUnitVal into basis.
Source project: Physlib
Person-level attribution pending.