def definition def or abbrev

`ofRatCore`

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

formal statement (Lean)

 106noncomputable def ofRatCore (q : ℚ) : LogicReal :=

Definition body.

 107  ⟨Completion.coe' (show CompareReals.Q from q)⟩
 108
 109/-- Embed a recovered rational into `LogicReal`. -/

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

Lean names referenced from this declaration's body.