THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This file defines
zsqrtd.to_real and related lemmas.
It is in a separate file to avoid pulling in all of
The image of
real.sqrt which takes the positive root of
If the negative root is desired, use
to_real h a.conj.