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 2,569 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.
Showing 859 to 864 of 2,569 results.
deriv_denom_zpow
Mathematical statement
Derivative of denom^(-k): d/dz[(cz+d)^(-k)] = -k * c * (cz+d)^(-k-1).
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
deriv_FmodGReal
Mathematical statement
The derivative of FmodGReal is (-2π) * L₁,₀(it) / G(it)².
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
deriv_moebius
Mathematical statement
Derivative of the Möbius transformation: d/dz[(az+b)/(cz+d)] = 1/(cz+d)². Uses det(γ) = 1: a(cz+d) - c(az+b) = ad - bc = 1.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
deriv_resToImagAxis_eq
Mathematical statement
Chain rule for restriction to imaginary axis: d/dt F(it) = -2π * (D F)(it). This connects the real derivative along the imaginary axis to the normalized derivative D. The key computation is: - The imaginary axis is parametrized by g(t) = I * t - By chain rule: d/dt F(it) = (dF/dz)(it) · (d/dt)(it) = F'(it) · I - Since D = (2πi)⁻¹ · d/dz, we have F' = 2π...
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
deriv_tanh
Mathematical statement
The derivative of tanh(x) is 1 - tanh(x)^2
Source project: Physlib
Person-level attribution pending.
det_muller_lang_concat
Mathematical statement
The concatenation of a regular language and a deterministic Muller language is a deterministic Muller language.
Source project: Automata Theory
Person-level attribution pending.