Commit 2021-02-06 22:54 7f467fad
View on Github →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.