PR #911 refactor(*): rename is_group_hom.mul to map_mul

refactor(*): rename is_group_hom.mul to map_mul #911

ChrisHughes24 merged 3 commits into master from is_group_hom

refactor(*): rename is_group_hom.mul to map_mul

142cdec2

jcommelin requested a review 6 years ago

Fix splits_mul

57b88934

ChrisHughes24 approved these changes on 2019-04-09

ChrisHughes24 added ready-to-merge

Merge branch 'master' into 'is_group_hom'

6433989b

ChrisHughes24 merged 66a86ffe into master 6 years ago

ChrisHughes24 deleted the is_group_hom branch 6 years ago

Reviewers

ChrisHughes24

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone