Hom

📁 Source: Mathlib/Algebra/Order/Archimedean/Hom.lean

Statistics

Metric	Count
Definitions	0
Theorems apply_eq_self, eq_id, subsingleton, apply_eq_self, eq_refl, subsingleton_left, subsingleton_right	7
Total	7

OrderRingHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_eq_self 📖	mathematical	—	DFunLike.coe OrderRingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instFunLike	—	eq_id
eq_id 📖	mathematical	—	id Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	subsingleton
subsingleton 📖	mathematical	—	OrderRingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	ext exists_rat_btwn lt_asymm Monotone.reflect_lt OrderHomClass.mono instOrderHomClass map_ratCast instRingHomClass Ne.lt_or_gt

OrderRingIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_eq_self 📖	mathematical	—	DFunLike.coe OrderRingIso Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Distrib.toAdd Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder EquivLike.toFunLike instEquivLike	—	OrderRingHom.apply_eq_self
eq_refl 📖	mathematical	—	refl Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Distrib.toAdd Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	subsingleton_left
subsingleton_left 📖	mathematical	—	OrderRingIso Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Distrib.toAdd Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Function.Injective.subsingleton Function.Bijective.injective symm_bijective subsingleton_right
subsingleton_right 📖	mathematical	—	OrderRingIso Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Distrib.toAdd Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Function.Injective.subsingleton toOrderRingHom_injective OrderRingHom.subsingleton

---

← Back to Index