Additive is_scalar_tower

Stream: Is there code for X?

[Yaël Dillies]

@Eric Wieser, do we not have the additive version of is_scalar_tower?

[Eric Wieser]

Don't think so

[Johan Commelin]

What exactly would that look like? What is the additive version of smul?

[Yakov Pechersky]

vadd

[Johan Commelin]

aah, of course :bulb:

[Yaël Dillies]

Do we want it?

[Yury G. Kudryashov]

Do you need it?

[Yury G. Kudryashov]

If yes, then add it.

[Yaël Dillies]

Not yet

[Yury G. Kudryashov]

IMHO, we shouldn't add it while nobody needs it.

[Kevin Buzzard]

We certainly need additive groups and multiplicative groups, but often in complex situations it's multiplicative things acting on additive things. I don't know all the times is_scalar_tower is used but in essentially all the ones I do know it's when you have three rings A,B,C and maps A->B->C inducing the smul. In this case the vadd scalar tower would be a theorem :-) but it doesn't really come up in practice, or at least it comes up way less than the smul version.

[Yury G. Kudryashov]

It is possible that we'll want to_additive on some theorem that uses is_scalar_tower under the hood. Then we'll add is_vadd_tower.

[Yaël Dillies]

Yeah, and when that day comes, we'll to additivize all the stuff we hadn't so far, which could turn out to be a pain if some lemmas along the way haven't been proved correctly. But again, we don't need it yet.