Conjneg

📁 Source: Mathlib/Algebra/Order/Star/Conjneg.lean

Statistics

Metric	Count
Definitions	0
Theorems conjneg_neg', conjneg_nonneg, conjneg_nonpos, conjneg_pos	4
Total	4

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
conjneg_neg' 📖	mathematical	—	Preorder.toLT Pi.preorder PartialOrder.toPreorder conjneg CommRing.toCommSemiring Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono Pi.instIsLeftCancelAdd AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Pi.isOrderedAddMonoid IsOrderedCancelAddMonoid.toIsOrderedAddMonoid IsOrderedAddMonoid.toIsOrderedCancelAddMonoid StarOrderedRing.toIsOrderedAddMonoid
conjneg_nonneg 📖	mathematical	—	Pi.hasLe Preorder.toLE PartialOrder.toPreorder Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring conjneg	—	Equiv.forall_congr' neg_neg
conjneg_nonpos 📖	mathematical	—	Pi.hasLe Preorder.toLE PartialOrder.toPreorder conjneg CommRing.toCommSemiring Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	IsOrderedAddMonoid.toAddLeftMono Pi.isOrderedAddMonoid IsOrderedCancelAddMonoid.toIsOrderedAddMonoid IsOrderedAddMonoid.toIsOrderedCancelAddMonoid StarOrderedRing.toIsOrderedAddMonoid
conjneg_pos 📖	mathematical	—	Preorder.toLT Pi.preorder PartialOrder.toPreorder Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring conjneg	—	—

---

← Back to Index