Commit 2025-12-08 21:44 7a954882

perf(Analysis.Complex.Exponential): make Complex.exp an irreducible_def (#32599) Recall that irreducible_def creates a declaration that is not unfolded by both the elaborator and the kernel (without some special effort). Currently, UpperHalfPlane.isometry_vertical_line takes a long time to type check in the kernel because it attempts to unfold Real.exp during whnf. Unfolding Real.exp quickly leads to unfolding Complex.exp. I don't think there is any good reason to want to unfold Complex.exp so this PR makes it an irreducible_def.