Mathlib Map

Theorems · Definition · number theory

Zsqrtd.casesOn

{d : ℤ} → {motive : ℤ√d → Sort u} → (t : ℤ√d) → ((re im : ℤ) → motive { re := re, im := im }) → motive t
Defined in
Mathlib.NumberTheory.Zsqrtd.Basic
Cited by
3 results in Mathlib
Foundations
Depth 4 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

GaussianInt.toComplex_inj · cited by 3GaussianInt.toComplex_injZsqrtd.hom_ext · cited by 1Zsqrtd.hom_extZsqrtd.noConfusion · cited by 0Zsqrtd.noConfusionZsqrtd.noConfusionType · cited by 0Zsqrtd.noConfusionTypeGaussianInt.intCast_complex_norm · cited by 0GaussianInt.intCast_compl…Zsqrtd · cited by 105ZsqrtdZsqrtd.casesOnCITED 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 by5

Results whose statement or proof uses this declaration.