Commit 2024-06-20 09:54 c6b786e2

View on Github →

chore: remove unnecessary nolint simpNFs (#13982) This arose in the context of this Zulip discussion. See also

  • #13889 for a previous hand-made version;
  • #13970 for the automatic detection of unnecessary nolint simpNFs, (at least locally unnecessary).

Estimated changes

modified theorem WithBot.bot_mul_bot
modified theorem WithTop.top_mul_top
modified theorem ENat.coe_mul
modified theorem Finset.insert_empty
modified theorem NNRat.coe_natCast
modified theorem NNRat.coe_one
modified theorem NNRat.coe_pow
modified theorem NNRat.coe_zero