IsScalarTower maze

Stream: maths

[Riccardo Brasca]

@Andrew Yang noted here that we may want various IsScalarTower results about four rings. Proving those result is not difficult, but maybe at some point we will need a version for five rings etc. The point is that the number of lemmas grows very quickly.

Does anyone think it would possible to write a tactic to solve these IsScalarTower issues?

[Riccardo Brasca]

Randomly tagging @Damiano Testa

[Damiano Testa]

Would possibly an extension of algebraize be useful here?

[Andrew Yang]

If there were a automated forward style proof searching tactic then this would be very useful here. Can aesop do this (AFAIK it search backwards?)

[Bhavik Mehta]

Aesop can do some forward reasoning, I don't know how reasonable it is to make a custom aesop set which has the forward lemmas as needed

[Andrew Yang]

I think (hope) that the four I mentioned is everything we need (and perhaps various IsScalarTower instances if reasonable)