Project-declaredLean 4.32.0
Tanh const mul has Temperate Growth
tanh_const_mul_hasTemperateGrowth
Plain-language statement
tanh(κx) has temperate growth
physicsquantum field theoryrelativity
Source project: Physlib
Person-level attribution pending.
Source-pinned research
Research proof index
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 filtersView proof record
Project-declaredLean 4.32.0
Tanh has Temperate Growth
tanh_hasTemperateGrowth
Plain-language statement
tanh has temperate growth
physicsquantum field theoryrelativity
Source project: Physlib
Person-level attribution pending.
Project-declaredLean 4.32.0
Chain rule T beta
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.
physicsquantum field theoryrelativity
Source project: Physlib
Person-level attribution pending.
Project-declaredLean 4.32.0
Contr T eval T
TensorSpecies.Tensor.contrT_evalT
Plain-language statement
Commuting evaluation with contraction. Evaluating index k and then contracting the pair i j equals contracting the corresponding pair k.succAbove i, k.succAbove j and then evaluating the residual index, up to the identity reindexing IsReindexing.succAbove_succSuccAbove_comm.
physicsquantum field theoryrelativity
Source project: Physlib
Person-level attribution pending.
Project-declaredLean 4.32.0
Eq sum eval T
TensorSpecies.Tensor.eq_sum_evalT
Plain-language statement
Reconstruction of a tensor from the evaluations of its last index: every t : Tensor S c is the sum over basis indices i of the evaluation evalT (Fin.last n) i t tensored with the basis covector basis ![c (Fin.last n)] (single.symm i), with the appended index permuted back into the last slot.
physicsquantum field theoryrelativity
Source project: Physlib
Person-level attribution pending.
Project-declaredLean 4.32.0
Eq sum eval T of single tensor basis
TensorSpecies.Tensor.eq_sum_evalT_of_single_tensor_basis
Plain-language statement
Basis expansion of a one-index tensor: every t : Tensor S ![c] is the sum over basis indices i of its evaluation coefficient toField (evalT 0 i t) times the corresponding basis tensor.
physicsquantum field theoryrelativity
Source project: Physlib
Person-level attribution pending.