Definitions: Mathlib.NumberTheory, part 3 of 3

Let $d$ be an integer. Then the elements of $\mathrm{Zsqrtd}$ applied to $d$ are a basic type.

x is nonnegative (from the name)

Let $x$ be an element of $\mathrm{Zsqrtd}$ applied to $d$. Then we can say that $x$ is nonnegative.

Let $c$ and $d$ be natural numbers. Let $x$ and $x_{1}$ be integers. Then we can say that $\operatorname{Nonnegg}$ holds for $c$, $d$, $x$ and $x_{1}$.

Let $x$ be a natural number. Then we can say that $\operatorname{Nonsquare}$ holds for $x$.

Let $a$, $c$, $b$ and $d$ be natural numbers. Then $\operatorname{SqLe}$ holds for $a$, $c$, $b$ and $d$, if $c \times a \times a \leq d \times b \times b$.

the imaginary part of self (from the name)

Let $\mathrm{self}$ be an element of $\mathrm{Zsqrtd}$ applied to $d$. Then the imaginary part of $\mathrm{self}$ is an integer defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the lift (from the name)

The lift is an equivalence from $\SubtypeSet {r}{(\EqtMACRoH {(r \times r)}{d})}$ to the set of ring homomorphisms of $\mathrm{Zsqrtd}$ applied to $d$ and $R$.

the norm of n (from the docstring)

Let $n$ be an element of $\mathrm{Zsqrtd}$ applied to $d$. Then the norm of $n$ is an integer defined as the difference between the product of the real part of $n$ and the real part of $n$ and the product of $d$, the imaginary part of $n$ and the imaginary part of $n$.

the norm monoid homomorphism (from the name)

The norm monoid homomorphism is a monoid homomorphism of $\mathrm{Zsqrtd}$ applied to $d$ and $\Integer$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{norm}$ and $\mathrm{Zsqrtd\_\_norm\_one}$ and $\mathrm{Zsqrtd\_\_norm\_mul}$.

Let $n$ be an integer. Then $\operatorname{ofInt}$ applied to $n$ is an element of $\mathrm{Zsqrtd}$ applied to $d$ defined as $\operatorname{mk}$ applied to $n$ and $0$.

the real part of self (from the name)

Let $\mathrm{self}$ be an element of $\mathrm{Zsqrtd}$ applied to $d$. Then the real part of $\mathrm{self}$ is an integer defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

$\operatorname{sqrtd}$ is an element of $\mathrm{Zsqrtd}$ applied to $d$ defined as $\operatorname{mk}$ applied to $0$ and $1$.

Gaussian integer (from the name)

A Gaussian integer is an element of $\mathrm{Zsqrtd}$ applied to $\operatorname{neg}$ applied to $1$.

the complex (from the name)

The complex is a ring homomorphism of the set of Gaussian integers and the set of complexes defined as $\operatorname{lift}$ applied to $\operatorname{I}$.

Assume that $0 \leq d$. Then $\operatorname{toReal}$ applied to $h$ is a ring homomorphism of $\mathrm{Zsqrtd}$ applied to $d$ and $\Real$ defined as $\operatorname{lift}$ applied to the square root of $d$.