Theorems · Inductive type · number theory
Zsqrtd
ℤ → Type
The ring of integers adjoined with a square root of d.
These have the form a + b √d where a b : ℤ. The components
are called re and im by analogy to the negative d case.
- Defined in
- Mathlib.NumberTheory.Zsqrtd.Basic
- Cited by
- 105 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 2 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by124
Results whose statement or proof uses this declaration.
- Zsqrtd.imstatement and proof · cited by 54
- Zsqrtd.restatement and proof · cited by 53
- Pell.Solution₁proof · cited by 50
- GaussianIntproof · cited by 37
- Zsqrtd.normstatement and proof · cited by 35
- Zsqrtd.extstatement and proof · cited by 18
- Zsqrtd.Nonnegstatement and proof · cited by 15
- Zsqrtd.im_intCaststatement · cited by 14
- Zsqrtd.re_intCaststatement · cited by 14
- Pell.pellZdstatement · cited by 13
- Zsqrtd.sqrtdstatement · cited by 11
- Pell.IsPellstatement and proof · cited by 9