-
Notifications
You must be signed in to change notification settings - Fork 259
/
ToReal.lean
34 lines (25 loc) · 1.06 KB
/
ToReal.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
/-
Copyright (c) 2021 Eric Wieser. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Eric Wieser
-/
import Mathlib.Data.Real.Sqrt
import Mathlib.NumberTheory.Zsqrtd.Basic
#align_import number_theory.zsqrtd.to_real from "leanprover-community/mathlib"@"e59154361202a34b26176e0de9267ef8e2dcd446"
/-!
# 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`.
-/
namespace Zsqrtd
/-- 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)`. -/
@[simps!]
noncomputable def toReal {d : ℤ} (h : 0 ≤ d) : ℤ√d →+* ℝ :=
lift ⟨√↑d, Real.mul_self_sqrt (Int.cast_nonneg.mpr h)⟩
#align zsqrtd.to_real Zsqrtd.toReal
theorem toReal_injective {d : ℤ} (h0d : 0 ≤ d) (hd : ∀ n : ℤ, d ≠ n * n) :
Function.Injective (toReal h0d) :=
lift_injective _ hd
#align zsqrtd.to_real_injective Zsqrtd.toReal_injective
end Zsqrtd