Ring

📁 Source: Mathlib/Order/Filter/Ring.lean

Statistics

Metric	Count
Definitions	0
Theorems add_le_add, mul_le_mul, mul_le_mul', mul_nonneg, instIsOrderedRing, eventually_sub_nonneg	6
Total	6

Filter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eventually_sub_nonneg 📖	mathematical	—	EventuallyLE Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	eventually_congr Eventually.of_forall sub_nonneg

Filter.EventuallyLE

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_le_add 📖	mathematical	Filter.EventuallyLE Preorder.toLE	Pi.instAdd	—	Filter.mp_mem Filter.univ_mem' add_le_add
mul_le_mul 📖	mathematical	Filter.EventuallyLE Preorder.toLE Pi.instZero MulZeroClass.toZero	Pi.instMul MulZeroClass.toMul	—	Filter.mp_mem Filter.univ_mem' mul_le_mul
mul_le_mul' 📖	mathematical	Filter.EventuallyLE Preorder.toLE	Pi.instMul	—	Filter.mp_mem Filter.univ_mem' mul_le_mul'
mul_nonneg 📖	mathematical	Filter.EventuallyLE Preorder.toLE PartialOrder.toPreorder Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	Filter.mp_mem Filter.univ_mem' mul_nonneg IsOrderedRing.toPosMulMono

Filter.Germ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsOrderedRing 📖	mathematical	—	IsOrderedRing Filter.Germ instSemiring instPartialOrder	—	instIsOrderedAddMonoid IsOrderedRing.toIsOrderedAddMonoid const_le zero_le_one IsOrderedRing.toZeroLEOneClass inductionOn inductionOn₂ Filter.Eventually.mp Filter.Eventually.mono mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono

---

← Back to Index