Theorem div_mul_comm
Modification history
2022-05-10 17:00
src/algebra/group/basic.lean
refactor(algebra/{group,group_with_zero/basic): Delete lemmas generalized to division monoids (#14042) …
Added div_mul_commView on Github →2022-03-03 19:27
src/algebra/group/basic.lean
chore(algebra/{group,group_with_zero}/basic): rename `div_mul_div` and `div_mul_comm` (#12365) …
Deleted div_mul_commView on Github →2021-09-06 12:25
src/algebra/group/basic.lean
feat(algebra/lattice_ordered_group): add basic theory of lattice ordered groups (#8673)
Added div_mul_commView on Github →