theorem proved term proof

`toComplex_re_eq`

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

formal statement (Lean)

  45theorem toComplex_re_eq (s : LogicComplex) :
  46    (toComplex s).re = RealsFromLogic.LogicReal.toReal s.re := rfl

Term-mode proof.

  47
  48/-- The Euler product theorem, read on recovered complex inputs. -/

Lean names referenced from this declaration's body.