Commit 2023-05-25 00:26 9b45a6f8

View on Github →

chore: restore simp tag for BoxIntegral.BoxAdditiveMap.map_split_add (#4294)

Estimated changes

Modified Mathlib/Analysis/BoxIntegral/Partition/Additive.lean

Modified Mathlib/Data/Option/Defs.lean

added theorem Option.elim'_none

added theorem Option.elim'_some