!bench

PR summary 407b6bffc3

Import changes for modified files

No significant changes to the import graph

Declarations diff

No declarations were harmed in the making of this PR! 🐙

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

./scripts/technical-debt-metrics.sh pr_summary

Here are the benchmark results for commit 407b6bf.
There were significant changes against commit da9df8d:

  Benchmark                             Metric         Change
  ===========================================================
+ ~Mathlib.RingTheory.Ideal.Cotangent   instructions   -21.6%
+ ~Mathlib.RingTheory.Kaehler.Basic     instructions    -6.2%

These two occurences were discovered because they timed out in another PR; maybe more are still hidden. Not sure who might know about more situations that could benefit from this. Maybe @erdOne?

I feel like this defeq abuse(?) happen very often (and I'm definitely guilty of many of them) that I unfortunately cannot give you a list of where it occurs.

This looks like a positive change, thanks!

bors merge

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style