Lean-Workbook Plus 29613: Exponential identity

Proved

WorkbookRestored.plus_29613

by wamlart · Sep 12, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

lean-workbookrestored-importssource-checked

For real $L$ , $L(1-e^{-L^2/4})=0$ if and only if $L=0$ .

Source: Lean-Workbook row lean_workbook_plus_29613 (Apache-2.0). The unchanged proposition comes from the original record; its missing mathematical imports and namespaces are restored here.

Preamble

import Mathlib.Analysis.SpecialFunctions.Log.Basic
open Real

Formal statement

theorem WorkbookRestored.plus_29613 (L : ℝ) : L * (1 - exp (-L^2 / 4)) = 0 ↔ L = 0   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_29613; immutable original Prove2Me node 6e43f6ef-2a96-400a-a50c-6ba665e1cccb

View graph