{z : ℂ} (hz : z ≠ 0) : phi 1 z = (Complex.exp z - 1) / z

-- Generated from ChapterH1.lean — theorem BookProof.ChapterH1.phi_one
import Mathlib
import Definitions.Def_ChapterH1
open BookProof.ChapterH1






open scoped BigOperators
open intervalIntegral


noncomputable section

theorem BookProof.ChapterH1.phi_one {z : ℂ} (hz : z ≠ 0) : phi 1 z = (Complex.exp z - 1) / z := by sorry