!bench

PR summary 0a0c535bcd

Import changes for modified files

No significant changes to the import graph

Declarations diff

- instance : FunLike (M ≃ₛₗ[σ] M₂) M M₂

## 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.

Here are the benchmark results for commit 4cc4221.
The entire run failed.
Found no significant differences.

!bench

Here are the benchmark results for commit 4cc4221.
The entire run failed.
Found no significant differences.

!bench

Here are the benchmark results for commit 4cc4221.
The entire run failed.
Found no significant differences.

!bench

Here are the benchmark results for commit 4cc4221.
The entire run failed.
Found no significant differences.

!bench

Here are the benchmark results for commit 4cc4221.
The entire run failed.
Found no significant differences.

!bench

Here are the benchmark results for commit 0a0c535.
There were significant changes against commit 12a1544:

  Benchmark                            Metric         Change
  ==========================================================
+ ~Mathlib.LinearAlgebra.TensorPower   instructions   -14.1%

Not sure how/if this interacts with #17870, but this one here is ready for review.

✌️ mo271 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

(It's still marked as a draft so I can't merge it.)

oops, marked as ready for review now...

bors r+

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style