modeq): add_div and others (#1689)

Commit

6 years ago

feat(data/nat/modeq): add_div and others (#1689) * feat(data/nat/modeq): add_div and others * remove unnecessary positivity assumptions. * fix build * brackets

References

#1689 - feat(data/nat/modeq): add_div and others

Author

ChrisHughes24

Committer

mergify[bot]

Parents

40de4fcb

mathlib 6ebb7e78 - feat(data/nat/modeq): add_div and others (#1689)

mathlib
6ebb7e78 - feat(data/nat/modeq): add_div and others (#1689)