theorem proved wrapper

`toComplex_add`

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

formal statement (Lean)

  92@[simp] theorem toComplex_add (z w : LogicComplex) :
  93    toComplex (z + w) = toComplex z + toComplex w := by

One-line wrapper that applies simp.

  94  simp [HAdd.hAdd, Add.add]
  95

Lean names referenced from this declaration's body.