[Merged by Bors] - feat(Algebra/IsScalarTower): add transitivity results

[xroblot]

Add the following:

Let `Q / P / N / M` be a scalar tower. If `P / N / M`, `Q / P / M` and `Q / P / N` are
scalar towers, then `Q / N / M` is also a scalar tower.

and variations.

Co-authored-by: Junyan Xu junyanxu.math@gmail.com

---

[github-actions]

PR summary a7cf25eee0

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ IsScalarTower.to₁₂₃
+ IsScalarTower.to₁₂₄
+ IsScalarTower.to₁₃₄
+ IsScalarTower.to₂₃₄

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.

---

No changes to technical debt.

You can run this locally as

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

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[Ruben-VandeVelde]

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

[alreadydone]

I have more general versions here (link updated). It's interesting to note the asymmetry between the required conditions for the two versions.

[Vierkantor]

@xroblot @alreadydone Are you okay with having both commits in this PR? Then I'll do a final review and get this merged.

[alreadydone]

Do you mean you want to merge my commit into this PR? I can open a pull request.

[Vierkantor]

Yes! That way we won't add something and then replace it immediately after. Your commit looks good to me, so I'd only like to make sure that the merge is good, and we can merge this PR.

[alreadydone]

I opened xroblot#1. Probably the docstrings need to be rewritten and added. I'm not sure about the trans in the names; I think to_left/to_right would be better.

[xroblot]

I am happy with whatever solution you think it's the best.

[Vierkantor]

Thanks! Let's get this merged, finally :)

bors r+

[mathlib-bors]

👎 Rejected by label

[xroblot]

@Vierkantor I think this PR needs another push

[Vierkantor]

Oops, let's try that again!

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• CI Success