Mathlib Map

Theorems · Definition · number theory

Zsqrtd.re

{d : ℤ} → ℤ√d → ℤ

Component of the integer not multiplied by √d

Defined in
Mathlib.NumberTheory.Zsqrtd.Basic
Cited by
53 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₁.x · cited by 42Solution₁.xZsqrtd.norm · cited by 35Zsqrtd.normZsqrtd.ext · cited by 18Zsqrtd.extZsqrtd.re_intCast · cited by 14Zsqrtd.re_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_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_…GaussianInt.toComplex_def₂ · cited by 2GaussianInt.toComplex_def₂Zsqrtd · cited by 105ZsqrtdZsqrtd.reCITED 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 by56

Results whose statement or proof uses this declaration.