mathlib

a8a616c5 - extract out the algebra_map definition when setting up algebra k (monoid_algebra k G)