mul vs map_mul

Stream: general

[Johan Commelin]

I noticed that is_group_hom has a field called mul, whereas I would expect it to be called map_mul. Similarly, in that namespace there is a lemma called one, and I would expect map_one. Etc...
Can/should these be renamed?

[Chris Hughes]

I think yes. Same for linear map, group action etc.

[Johan Commelin]

Or maybe I have wrong expectations...