Mathlib Map

Theorems · Definition · number theory

Zsqrtd.im

{d : ℤ} → ℤ√d → ℤ

Component of the integer multiplied by √d

Defined in
Mathlib.NumberTheory.Zsqrtd.Basic
Cited by
54 results in Mathlib
Foundations
Depth 2 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Pell.Solution₁.y · cited by 40Solution₁.yZsqrtd.norm · cited by 35Zsqrtd.normZsqrtd.ext · cited by 18Zsqrtd.extZsqrtd.im_intCast · cited by 14Zsqrtd.im_intCastZsqrtd.norm_eq_mul_conj · cited by 5Zsqrtd.norm_eq_mul_conjZsqrtd.norm_mul · cited by 4Zsqrtd.norm_mulGaussianInt.intCast_real_norm · cited by 4GaussianInt.intCast_real_…Zsqrtd.norm_nonneg · cited by 3Zsqrtd.norm_nonnegGaussianInt.intCast_im · cited by 3GaussianInt.intCast_imGaussianInt.intCast_re · cited by 3GaussianInt.intCast_reZsqrtd.ext_iff · cited by 3Zsqrtd.ext_iffZsqrtd.lift · cited by 3Zsqrtd.liftZsqrtd.norm_def · cited by 2Zsqrtd.norm_defGaussianInt.div_def · cited by 2GaussianInt.div_defGaussianInt.sq_add_sq_of_nat_prime_of_not_irreducible · cited by 2GaussianInt.sq_add_sq_of_…Zsqrtd · cited by 105ZsqrtdZsqrtd.imCITED BYCITES

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Zsqrtdstatement and proof · cited by 105

Cited by57

Results whose statement or proof uses this declaration.