Commit 2024-07-25 01:10 daf323c3

View on Github →

feat(Data/Set/Basic, Order/RelClasses): add @[simp] to subset_refl and subset_empty_iff (#15110) As per the description.

Estimated changes

Modified Mathlib/Data/Finset/Basic.lean

Modified Mathlib/Data/Set/Basic.lean

Modified Mathlib/MeasureTheory/Decomposition/SignedHahn.lean

Modified Mathlib/Order/Filter/CardinalInter.lean

Modified Mathlib/Order/RelClasses.lean

Modified Mathlib/Topology/Algebra/Group/Basic.lean