Image of `zsqrtd` in `ℝ` #

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 data.real into data.zsqrtd.

noncomputable def zsqrtd.to_real {d : ℤ} (h : 0 ≤ 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

@[simp]

theorem zsqrtd.to_real_apply {d : ℤ} (h : 0 ≤ d) (a : ℤ√d) :

theorem zsqrtd.to_real_injective {d : ℤ} (h0d : 0 ≤ d) (hd : ∀ (n : ℤ), d ≠ n * n) :

Image of zsqrtd in ℝ #