Commit 2024-03-30 17:52 573fa600

View on Github →

chore: mark EventuallyEq.refl as simp (#11475) Fixes #11441.

Estimated changes

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean

Modified Mathlib/Order/Filter/Basic.lean

Modified Mathlib/Order/Filter/Germ.lean

Modified Mathlib/Probability/Martingale/Basic.lean