112def conformal_remainder (t : ℝ) : ℝ := Real.exp t - 1 - t - t ^ 2 / 2
proof body
Definition body.
113 114/-- The second-order conformal expansion. This is *exact* with the 115 remainder explicitly named: it is just the rearrangement of 116 `exp(t) = 1 + t + t²/2 + R(t)`. -/
used by (4)
From the project-wide theorem graph. These declarations reference this one in their body.