mathlib3
eae6ae37 - feat(algebra/associated): add decidable instances (#12230)

Commit
3 years ago
feat(algebra/associated): add decidable instances (#12230) Makes equality and divisibility decidable in `associates`, given that divisibility is decidable in the general case. Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>
Author
Parents
Loading