Project-declaredLean 4.32.0
Deriv tanh
deriv_tanh
Plain-language statement
The derivative of tanh(x) is 1 - tanh(x)^2
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 6 research declarations. Search 10,000 more complete Mathlib declarations.
6 results
Clear filtersView proof record
Project-declaredLean 4.32.0
Iterated Deriv tanh const mul
iteratedDeriv_tanh_const_mul
Plain-language statement
Iterated derivative for scaled tanh
physicsquantum field theoryrelativity
Source project: Physlib
Person-level attribution pending.
Project-declaredLean 4.32.0
Iterated Deriv tanh is polynomial of tanh
iteratedDeriv_tanh_is_polynomial_of_tanh
Plain-language statement
The nth derivative of Tanh(x) is a polynomial of Tanh(x)
physicsquantum field theoryrelativity
Source project: Physlib
Person-level attribution pending.
Project-declaredLean 4.32.0
Polynomial tanh bounded
polynomial_tanh_bounded
Plain-language statement
For a polynomial P, show that P (tanh x) is bounded on the real line
physicsquantum field theoryrelativity
Source project: Physlib
Person-level attribution pending.
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.
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.