Commit 2024-06-27 21:04 76bb4257

View on Github →

chore(Order/Filter/Basic): assert_not_exists OrderedSemiring (#14179)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean

Modified Mathlib/Order/Filter/Basic.lean

deleted theorem Filter.EventuallyLE.mul_le_mul'

deleted theorem Filter.EventuallyLE.mul_le_mul

deleted theorem Filter.EventuallyLE.mul_nonneg

deleted theorem Filter.eventually_sub_nonneg

Modified Mathlib/Order/Filter/Extr.lean

Modified Mathlib/Order/Filter/FilterProduct.lean

Modified Mathlib/Order/Filter/Germ.lean

Created Mathlib/Order/Filter/Ring.lean

added theorem Filter.EventuallyLE.mul_le_mul'

added theorem Filter.EventuallyLE.mul_le_mul

added theorem Filter.EventuallyLE.mul_nonneg

added theorem Filter.eventually_sub_nonneg