Commit 2025-12-02 17:23 1d4d380b

View on Github →

chore: golf using simpa (#32349) Trace profiling results (shown if ≥10 ms before or after):

  • CharP.ringChar_ne_one: <10 ms before, <10 ms after 🎉
  • IsUltrametricDist.isNonarchimedean_nnnorm: 30 ms before, <10 ms after 🎉
  • SimpleGraph.sdiff_compl_neighborFinset_inter_eq: <10 ms before, 12 ms after
  • List.get_eq_get_rotate: <10 ms before, <10 ms after 🎉
  • MeasureTheory.IsSetRing.finsetSup_mem: 15 ms before, 27 ms after This golfing PR is batched under the following guidelines:
  • Up to 5 changed files per PR
  • Up to 25 changed declarations per PR
  • Up to 100 changed lines per PR

Estimated changes