mathlib3
feat(algebraic_geometry/prime_spectrum): prime spectrum of a ring is compact
#1987
Merged
Overview
Commits
28
Changes
View On GitHub

feat(algebraic_geometry/prime_spectrum): prime spectrum of a ring is compact #1987

mergify merged 28 commits into master from spec-compact
jcommelin
jcommelin wip
62942aaa
jcommelin wip
06e243c3
jcommelin Merge branch 'master' into spec-compact
5e8be377
jcommelin wip
c79b4d6c
jcommelin wip
c5312ea6
jcommelin WIP
3a3e963d
jcommelin Merge branch 'master' into refactor-compact
302f9463
jcommelin WIP
f5106eb8
jcommelin Reset changes that belong to other PR
e6026b88
jcommelin Docstrings
a2ccef69
jcommelin Add Heine--Borel to docstring
03282d06
jcommelin Cantor's intersection theorem
b5841d83
jcommelin Cantor for sequences
c7c714b6
jcommelin Merge branch 'lean-3.5.1' into spec-compact
a6067493
jcommelin Revert "Reset changes that belong to other PR"
08e0a658
jcommelin Move submodule lemmas to other file
f8461a92
jcommelin Fix build
1a040d1d
jcommelin jcommelin added blocked-by-other-PR
jcommelin Update prime_spectrum.lean
accfdf79
jcommelin Docstring
25623e99
jcommelin Merge branch 'master' into spec-compact
c38eb120
jcommelin jcommelin removed blocked-by-other-PR
jcommelin jcommelin added awaiting-review
jcommelin Merge branch 'master' into spec-compact
34292f60
jcommelin Update prime_spectrum.lean
cd78cab3
sgouezel
sgouezel commented on 2020-02-21
sgouezel
sgouezel commented on 2020-02-21
jcommelin Slight improvement?
7e86ac85
jcommelin Slightly improve structure of proof
81aeb280
sgouezel sgouezel removed awaiting-review
sgouezel sgouezel added ready-to-merge
sgouezel
sgouezel approved these changes on 2020-02-21
jcommelin jcommelin removed ready-to-merge
jcommelin jcommelin added WIP
jcommelin WIP
845d5d51
jcommelin Cleaning up proofs
8d0e4a63
jcommelin jcommelin removed WIP
jcommelin jcommelin added awaiting-review
jcommelin Final fixes
d18bc32d
sgouezel sgouezel removed awaiting-review
sgouezel sgouezel added ready-to-merge
mergify[bot] Merge branch 'master' into spec-compact
f8898e29
mergify mergify merged ea149c8d into master 5 years ago
mergify mergify deleted the spec-compact branch 5 years ago

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
No one assigned
Labels
ready-to-merge
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum