Image of Zsqrtd
in ℝ
#
This file defines Zsqrtd.toReal
and related lemmas.
It is in a separate file to avoid pulling in all of Data.Real
into Data.Zsqrtd
.
Zsqrtd
in ℝ
#This file defines Zsqrtd.toReal
and related lemmas.
It is in a separate file to avoid pulling in all of Data.Real
into Data.Zsqrtd
.