mathlib documentation

data.zsqrtd.to_real

Image of zsqrtd in ℝ #

This file defines zsqrtd.to_real and related lemmas. It is in a separate file to avoid pulling in all of data.real into data.zsqrtd.

source
def zsqrtd.to_real {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 to_real h a.conj.

Equations
source
@[simp]
theorem zsqrtd.to_real_apply {d : ℤ} (h : 0 ≤ d) (a : ℤ√d) :
⇑(zsqrtd.to_real h) a = ↑(a.re) + (↑(a.im)) * real.sqrt ↑d
source
theorem zsqrtd.to_real_injective {d : ℤ} (h0d : 0 ≤ d) (hd : ∀ (n : ℤ), d ≠ n * n) :
function.injective ⇑(zsqrtd.to_real h0d)