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.

@[simp]

theorem Zsqrtd.toReal_apply {d : ℤ} (h : 0 ≤ d) (a : ℤ√d) : (Zsqrtd.toReal h) a = ↑a.re + ↑a.im * Real.sqrt ↑d

noncomputable def Zsqrtd.toReal {d : ℤ} (h : 0 ≤ d) : ℤ√d →+* ℝ

The image of Zsqrtd in ℝ, using Real.sqrt which takes the positive root of d.

If the negative root is desired, use toReal h (star a).

Equations

• Zsqrtd.toReal h = Zsqrtd.lift { val := Real.sqrt ↑d, property := (_ : Real.sqrt ↑d * Real.sqrt ↑d = ↑d) }

theorem Zsqrtd.toReal_injective {d : ℤ} (h0d : 0 ≤ d) (hd : ∀ (n : ℤ), d ≠ n * n) : Function.Injective ⇑(Zsqrtd.toReal h0d)