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 187 research declarations. Search 10,000 more complete Mathlib declarations.
187 results
Clear filtersSUSY.N1.repr_conjChiralCovector
Plain-language statement
Component formula for the holomorphic covector conjugate: the ![I] basis component of conjChiralCovector t is the complex conjugate of the ![I] component of t.
Source project: Physlib
Person-level attribution pending.
SUSY.N1.toField_conjScalar
Plain-language statement
For scalar tensors, toField of the normalized tensor conjugate is the complex conjugate of toField.
Source project: Physlib
Person-level attribution pending.
Temperature.chain_rule_T_beta
Plain-language statement
Chain rule for β(T) : d/dT F(β(T)) = F'(β(T)) * (-1 / (kB * T^2)), within Ioi 0.
Source project: Physlib
Person-level attribution pending.
Verifier.id_knowledgeSoundness
Plain-language statement
The identity / trivial verifier is perfectly knowledge sound.
Source project: ArkLib
Person-level attribution pending.
Θ₂_imag_axis_re_pos
Plain-language statement
Θ₂(It) has positive real part for t > 0. Proof: Each term Θ₂_term n (It) = exp(-π(n+1/2)²t) is a positive real. The sum of positive reals is positive.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
Θ₂_term_imag_axis_re
Plain-language statement
Each term Θ₂_term n (I*t) has positive real part equal to exp(-π(n+1/2)²t) for t > 0.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.