Hom

📁 Source: Mathlib/Data/Real/Hom.lean

Statistics

Metric	Count
Definitions unique	1
Theorems nonemptyOrderRingHom, ringHom_apply, ringHom_monotone	3
Total	4

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nonemptyOrderRingHom 📖	mathematical	—	OrderRingHom Real Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder semiring instPreorder	—	instIsStrictOrderedRing
ringHom_apply 📖	mathematical	—	DFunLike.coe Real	—	DFunLike.congr_fun Unique.eq_default

Real.RingHom

Definitions

Name	Category	Theorems
unique 📖	CompOp	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ringHom_monotone 📖	mathematical	IsSquare Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	Monotone PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder DFunLike.coe RingHom Semiring.toNonAssocSemiring Ring.toSemiring RingHom.instFunLike	—	monotone_iff_map_nonneg RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass mul_self_nonneg AddGroup.existsAddOfLE IsOrderedAddMonoid.toAddLeftMono

---

← Back to Index