Commit 2020-08-10 19:28 4a75df92

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