Theorem LindemannWeierstrass.P_le_aux

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_le_aux View on Github →