Commit 2023-02-28 20:37 77e63150

View on Github →

feat: add to_additive linter checking whether additive decl exists (#1881)

  • Force the user to specify whether the additive declaration already exists.
  • Will raise a linter error if the user specified it wrongly
  • Requested on Zulip

Estimated changes

deleted theorem Finset.sum_Ico_succ_top
modified theorem Equiv.mulLeft_mul
modified theorem Equiv.mulLeft_one
modified theorem Equiv.mulRight_mul
modified theorem Equiv.mulRight_one