Theorems · Definition · number theory
Zsqrtd.lift
{R : Type u_1} → [inst : CommRing R] → {d : ℤ} → { r // r * r = ↑d } ≃ (ℤ√d →+* R)The unique RingHom from ℤ√d to a ring R, constructed by replacing √d with the provided
root. Conversely, this associates to every mapping ℤ√d →+* R a value of √d in R.
- Defined in
- Mathlib.NumberTheory.Zsqrtd.Basic
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 47 from the axioms · uses propext, Quot.sound
- Assumes
- CommRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- CommRingstatement and proof · cited by 17,173
- RingHomstatement and proof · cited by 10,189
- Equivstatement · cited by 8,337
- Zsqrtdstatement and proof · cited by 105
- Zsqrtd.improof · cited by 54
- Zsqrtd.reproof · cited by 53
- Zsqrtd.sqrtdproof · cited by 11
Cited by5
Results whose statement or proof uses this declaration.
- GaussianInt.toComplexproof · cited by 23
- Zsqrtd.toRealproof · cited by 2
- Zsqrtd.lift_apply_applystatement and proof · cited by 1
- Zsqrtd.lift_injectivestatement and proof · cited by 1
- Zsqrtd.lift_symm_apply_coestatement and proof · cited by 0