ToReal

📁 Source: Mathlib/NumberTheory/Zsqrtd/ToReal.lean

Statistics

Metric	Count
Definitions toReal	1
Theorems toReal_apply, toReal_injective	2
Total	3

Zsqrtd

Definitions

Name	Category	Theorems
toReal 📖	CompOp	2 math math: toReal_apply, toReal_injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toReal_apply 📖	mathematical	—	DFunLike.coe RingHom Zsqrtd Real Semiring.toNonAssocSemiring instSemiring Real.semiring RingHom.instFunLike toReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing AddGroupWithOne.toIntCast Ring.toAddGroupWithOne CommRing.toRing re Distrib.toMul im Real.sqrt Real.instIntCast	—	—
toReal_injective 📖	mathematical	—	Zsqrtd Real DFunLike.coe RingHom Semiring.toNonAssocSemiring instSemiring Real.semiring RingHom.instFunLike toReal	—	lift_injective IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing

---

← Back to Index