Scalar tower of algebras

Stream: Is there code for X?

[Heather Macbeth]

Does this lemma exist somewhere, relating the algebra_maps of a tower of three algebras?

import algebra.algebra.basic

variables {R : Type*} [comm_semiring R]
variables (S : Type*) [comm_semiring S]
variables {A : Type*} [ring A]
variables [algebra R S] [algebra S A] [algebra R A] [is_scalar_tower R S A]

example : algebra_map R A = (algebra_map S A).comp (algebra_map R S) :=
by ext r; simpa [algebra.smul_def] using (smul_assoc r (1:S) (1:A)).symm

[Riccardo Brasca]

docs#is_scalar_tower.algebra_map_eq

[Kevin Buzzard]

I think Heather's proof is better ;-)

[Heather Macbeth]

@Riccardo Brasca thank you!