mathlib3
551cf8e2 - refactor(algebra/associates): unite `associates.prime` with `prime` (#3988)

Commit

5 years ago

refactor(algebra/associates): unite `associates.prime` with `prime` (#3988) deletes `associates.prime`, replaces it with the existing `prime`

References

Author

awainverse

Parents