This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

feat(data/equiv/algebra) ring_equiv #533

Merged

digama0 merged 1 commit into leanprover-community:master from leanprover-fork:ring-equiv

Dec 20, 2018

Collaborator

kckennylau commented Dec 19, 2018

TO CONTRIBUTORS:

Make sure you have:

reviewed and applied the coding style: coding, naming
for tactics:
- added or adapted documentation in tactics.md
- write an example of use of the new feature in tactics.lean
make sure definitions and lemmas are put in the right files
make sure definitions and lemmas are not redundant

For reviewers: code review check list


          feat(data/equiv/algebra) ring_equiv

9042b60

digama0 merged commit f7697ce into leanprover-community:master

digama0 deleted the ring-equiv branch

December 20, 2018 13:12

cipher1024 pushed a commit that referenced this pull request


          feat(data/equiv/algebra): ring_equiv (#533)

0b71d48

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Labels

None yet