Mathlib Map

Theorems · Theorem · number theory

Zsqrtd.ext

∀ {d : ℤ} {x y : ℤ√d}, x.re = y.re → x.im = y.im → x = y
Defined in
Mathlib.NumberTheory.Zsqrtd.Basic
Cited by
18 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Zsqrtd.norm_eq_mul_conj · cited by 5Zsqrtd.norm_eq_mul_conjPell.Solution₁.ext · cited by 4Solution₁.extZsqrtd.smul_val · cited by 3Zsqrtd.smul_valZsqrtd.ext_iff · cited by 3Zsqrtd.ext_iffZsqrtd.decompose · cited by 2Zsqrtd.decomposePell.pellZd_succ · cited by 1Pell.pellZd_succPell.pellZd_succ_succ · cited by 1Pell.pellZd_succ_succZsqrtd.nsmul_val · cited by 1Zsqrtd.nsmul_valGaussianInt.mod_four_eq_three_of_nat_prime_of_prime · cited by 1GaussianInt.mod_four_eq_t…Zsqrtd.muld_val · cited by 1Zsqrtd.muld_valZsqrtd.norm_eq_zero_iff · cited by 0Zsqrtd.norm_eq_zero_iffPell.Solution₁.coe_mk · cited by 0Solution₁.coe_mkZsqrtd.ofInt_eq_intCast · cited by 0Zsqrtd.ofInt_eq_intCastZsqrtd.intCast_val · cited by 0Zsqrtd.intCast_valZsqrtd.isCoprime_of_dvd_isCoprime · cited by 0Zsqrtd.isCoprime_of_dvd_i…Zsqrtd · cited by 105ZsqrtdZsqrtd.im · cited by 54Zsqrtd.imZsqrtd.re · cited by 53Zsqrtd.reZsqrtd.extCITED BYCITES

Cites3

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

  • Zsqrtdstatement and proof · cited by 105
  • Zsqrtd.imstatement and proof · cited by 54
  • Zsqrtd.restatement and proof · cited by 53

Cited by18

Results whose statement or proof uses this declaration.