prod): `prod.swap` commutes with arithmetic (#12367)

Commit

3 years ago

chore(algebra/group/prod): `prod.swap` commutes with arithmetic (#12367) This also adds some missing `div` lemmas using `to_additive`.

Author

eric-wieser

Parents