Theorem LindemannWeierstrass.P_eq_integral_exp_mul_eval

Modification history

2026-09-07 07:56

Mathlib/NumberTheory/Transcendental/Lindemann/AnalyticalPart.lean

chore(NumberTheory/Transcendental/Lindemann/AnalyticalPart): automated extraction from #28013 (#43515) …

Added LindemannWeierstrass.P_eq_integral_exp_mul_eval View on Github →