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 filtersQuantumMechanics.SpaceDHilbertSpace.mulOperator_hasDenseDomain
Plain-language statement
The multiplication operator corresponding to a μ-a.e. strongly measurable function is densely defined.
Source project: Physlib
Person-level attribution pending.
QuantumMechanics.SpaceDHilbertSpace.mulOperator_smul_ge
Plain-language statement
Scalar multiplication and mulOperator commute except possibly for c = 0 where the domains of 0 • 𝓜 μ f and 𝓜 μ 0 = 0 may not agree. See mulOperator_smul_eq for equality when c ≠ 0.
Source project: Physlib
Person-level attribution pending.
QuantumMechanics.SpaceDHilbertSpace.SchwartzSubmodule.zero_eq_top
Project documentation
The linear equivalence between the Schwartz maps 𝓢(Space d, ℂ) and the Schwartz submodule of SpaceDHilbertSpace d μ. -/ def schwartzEquiv {d : ℕ} (μ : Measure (Space d)) [μ.HasTemperateGrowth] [μ.IsOpenPosMeasure] : 𝓢(Space d, ℂ) ≃ₗ[ℂ] SchwartzSubmodule d μ := LinearEquiv.ofInjective (schwartzIncl μ).toLinearMap (injective_toLp 2 μ) namespace Schwar...
Source project: Physlib
Person-level attribution pending.
realLorentzTensor.coMetric_repr_apply_eq_minkowskiMatrix
Project documentation
The tensor contrMetric is invariant under the action of LorentzGroup d. -/ @[simp] lemma actionT_contrMetric {d} (g : LorentzGroup d) : g • η d = η d := by erw [TensorSpecies.metricTensor_invariant] /- ## There value with respect to a basis
Source project: Physlib
Person-level attribution pending.
realLorentzTensor.contrT_toComplex
Plain-language statement
The map toComplex commutes with contrT.
Source project: Physlib
Person-level attribution pending.
realLorentzTensor.evalT_toComplex
Plain-language statement
The map toComplex commutes with evalT.
Source project: Physlib
Person-level attribution pending.