mul_add): add lemmas about multiplication and addition on a group being bijective and finite cancel_monoid_with_zeros (#10046)

Commit

4 years ago

feat(data/equiv/mul_add): add lemmas about multiplication and addition on a group being bijective and finite cancel_monoid_with_zeros (#10046)

Author

alexjbest

Parents