mathlib3 documentation


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.

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) :