mathlib

4a75df92 - feat(group_theory/group_action): generalize `is_algebra_tower` (#3717)

feat(group_theory/group_action): generalize `is_algebra_tower` (#3717) This PR introduces a new typeclass `is_scalar_tower R M N` stating that scalar multiplications between the three types are compatible: `smul_assoc : ((x : R) • (y : M)) • (z : N) = x • (y • z)`. This typeclass is the general form of `is_algebra_tower`. It also generalizes some of the existing instances of `is_algebra_tower`. I didn't try very hard though, so I might have missed some instances. Related Zulip discussions: * https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Effect.20of.20changing.20the.20base.20field.20on.20span * https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/pull.20back.20an.20R.20module.20along.20.60S.20-.3E.2B*.20R.60