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 filtersGroupTheory.SO3.exists_stationary_vec
Plain-language statement
For every element of SO(3) there exists a vector which remains unchanged under the action of that SO(3) element.
Source project: Physlib
Person-level attribution pending.
HasVarAdjoint.unique
Plain-language statement
Variational adjoint is unique only when applied to smooth functions.
Source project: Physlib
Person-level attribution pending.
IdealGas.partitionZ_eq
Plain-language statement
The partition function Z for an ideal gas.
Source project: Physlib
Person-level attribution pending.
integral_isDimensionallyCorrect
Plain-language statement
The statement that for a measure μ of dimension d, and a function f : M → G of dimension (CarriesDimension.d G * d⁻¹) (where CarriesDimension.d G is the dimension associated with terms of type G), then ∫ x, f x ∂μ has the correct dimension, namely CarriesDimension.d G. In other words, the function: ``` fun (μ : DimSet (MeasureTheory.Measu...
Source project: Physlib
Person-level attribution pending.
iteratedDeriv_tanh_const_mul
Plain-language statement
Iterated derivative for scaled tanh
Source project: Physlib
Person-level attribution pending.
iteratedDeriv_tanh_is_polynomial_of_tanh
Plain-language statement
The nth derivative of Tanh(x) is a polynomial of Tanh(x)
Source project: Physlib
Person-level attribution pending.