`BookProof.ChapterCoherentThermalFidelity.coherentThermalFidelity_vacuum` (lam : ℝ) : coherentThermalFidelity 0 lam = Real.exp (-lam)

Initializing...

`BookProof.ChapterCoherentThermalFidelity.coherentThermalFidelity_vacuum` (lam : ℝ) : coherentThermalFidelity 0 lam = Real.exp (-lam) · Prove2Me