def definition def or abbrev

`ofLogicRat`

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

formal statement (Lean)

 127def ofLogicRat (q : RationalsFromLogic.LogicRat) : LogicComplex :=

Definition body.

 128  ofLogicReal (RealsFromLogic.LogicReal.ofLogicRat q)
 129

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

toComplex_ofLogicRat in IndisputableMonolith.Foundation.ComplexFromLogic decl_use
ofLogicRat in IndisputableMonolith.Foundation.RealsFromLogic decl_use
toReal_ofLogicRat in IndisputableMonolith.Foundation.RealsFromLogic decl_use

Lean names referenced from this declaration's body.