feat(algebra/group/hom): add inv_comp and comp_inv (#6046)
Two missing lemmas. Used in the Liquid Tensor Experiment.
Inversion for monoid hom is (correctly) only defined when the target is a comm_group; this explains the choice of typeclasses. I follow `inv_apply` and use `{}` rather than `[]`, but this is certainly not my area of expertise.
