Theorem LindemannWeierstrass.hasDerivAt_cexp_mul_sumIDeriv

Modification history

2024-12-21 09:59
Mathlib/NumberTheory/Transcendental/Lindemann/Init/AnalyticalPart.lean
feat: analytic part of Lindemann-Weierstrass (#20092)
Added LindemannWeierstrass.hasDerivAt_cexp_mul_sumIDerivView on Github →