Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-25 16:06 089d0586

View on Github →

feat(tactic/lint): linter for commutativity lemmas that are marked simp (#2045)

  • feat(tactic/lint): linter for commutativity lemmas that are marked simp
  • chore(*): remove simp from commutativity lemmas
  • doc(*): document simp_comm linter

Estimated changes

modified theorem finmap.erase_erase
modified theorem finset.inter_comm
modified theorem finset.inter_left_comm
modified theorem finset.inter_right_comm
modified theorem finset.union_comm
modified theorem alist.erase_erase
modified theorem list.disjoint_comm
modified theorem multiset.disjoint_comm
modified theorem nat.dist_comm