[Merged by Bors] - feat(Archive/Imo): formalize IMO 1961q3

[urkud]

---

• depends on: [Merged by Bors] - feat(Parity): add lemmas about x ^ n = ±y ^ n #9881
• depends on: [Merged by Bors] - feat(Trigonometric): add lemmas about cos x = -1 ↔ _ etc #9878

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(Parity): add lemmas about x ^ n = ±y ^ n #9881
• [Merged by Bors] - feat(Trigonometric): add lemmas about cos x = -1 ↔ _ etc #9878
  By Dependent Issues (🤖). Happy coding!

[grunweg]

Is this PR ready for review?

[urkud]

Some docs are missing and I have no time to write them.

[github-actions]

PR summary 7cd26f3f6d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ Imo1961Q3
+ abs_cos_int_mul_pi

You can run this locally as follows

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

[joneugster]

It appears to me that this PR is in a reasonably good shape and it would be more desirable to have it in Archive as-is instead of waiting for more documentation (it's also not clear to me what documentation is supposedly missing). I suggest

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by joneugster.

[sgouezel]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style