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

feat(ring_theory/subring): ring.closure #444

Merged
merged 1 commit into from
Nov 5, 2018
Merged

feat(ring_theory/subring): ring.closure #444

merged 1 commit into from
Nov 5, 2018

Conversation

kckennylau
Copy link
Collaborator

TO CONTRIBUTORS:

Make sure you have:

  • reviewed and applied the coding style: coding, naming
  • for tactics:
  • 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

@kckennylau kckennylau changed the title feature(ring_theory/subring): ring.closure feat(ring_theory/subring): ring.closure Oct 28, 2018
@digama0 digama0 merged commit 8ae3fb8 into leanprover-community:master Nov 5, 2018
@digama0 digama0 deleted the ring-closure branch November 5, 2018 14:03
jdsalchow pushed a commit to jdsalchow/mathlib that referenced this pull request Dec 8, 2018
@kckennylau @jdsalchow
feat(ring_theory/subring): ring.closure (leanprover-community#444)
aecc746
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@kckennylau @digama0