theorem proved wrapper

`toReal_add`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 138@[simp] theorem toReal_add (x y : LogicReal) : toReal (x + y) = toReal x + toReal y :=

One-line wrapper that applies toReal_fromReal.

 139  toReal_fromReal _

From the project-wide theorem graph. These declarations reference this one in their body.

coshL_eq_exp in IndisputableMonolith.Foundation.LogicRealTranscendentals decl_use

Lean names referenced from this declaration's body.