[Merged by Bors] - feat: add Algebra ℝ A instance given Algebra ℂ A

[j-loreaux]

---

• depends on: [Merged by Bors] - feat: port test/instance_diamonds.lean #9037

[eric-wieser]

!bench

[leanprover-bot]

Here are the benchmark results for commit 123b74b.
There were significant changes against commit bbc6e56:

  Benchmark      Metric       Change
  ==================================
- open Mathlib   wall-clock     5.6%

[eric-wieser]

Quoting a private message:

Note: for #8991 this also works:

import Mathlib

variable {A} [Ring A] [Algebra ℝ A]
open Algebra TensorProduct

example : (leftAlgebra : Algebra ℂ (ℂ ⊗[ℝ] A)).complexToReal = leftAlgebra := rfl

I'd like to see this committed too. It can go in test/instance_diamonds.lean once #9037 goes in

[eric-wieser]

bors d+

[mathlib-bors]

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

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• [Merged by Bors] - feat: port test/instance_diamonds.lean #9037
  By Dependent Issues (🤖). Happy coding!

[eric-wieser]

bors merge

Thanks!

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Lint style
• Check all files imported
• Build