mathlib3
e5e0ae74 - chore(data/set/intervals/image_preimage): remove unnecessary add_comm in lemmas (#7276)

Commit
4 years ago
chore(data/set/intervals/image_preimage): remove unnecessary add_comm in lemmas (#7276) These lemmas introduce an unexpected flip of the addition, whereas without these lemmas the simplification occurs as you might expect. Since these lemmas aren't otherwise used in mathlib, it seems simplest to just remove them. Let me know if I'm missing something, or some reason to prefer flipping the addition. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Parents
Loading