leanprover-community lean-perfectoid-spaces issues

leanprover-community / lean-perfectoid-spaces

Perfectoid spaces in the Lean formal theorem prover.

https://leanprover-community.github.io/lean-perfectoid-spaces/

Apache License 2.0

115 stars 12 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

Add publication to landing page

#69 jcommelin closed 2 years ago
0
migrate CI from Travis to GitHub actions

#68 bryangingechen opened 3 years ago
1
update elan URL

#67 bryangingechen closed 3 years ago
3
PR into mathlib

#66 kckennylau opened 4 years ago
1
Bump lean to 3.5.1

#65 jcommelin closed 4 years ago
0
Mathlib bump

#64 jcommelin closed 4 years ago
0
Definition of nondiscrete valuations

#63 jcommelin opened 4 years ago
0
Towards an example of a perfectoid field

#62 jcommelin opened 4 years ago
0
Doc doc doc — add docstrings to all defs

#61 jcommelin closed 4 years ago
0
Spa refactor

#60 jcommelin closed 4 years ago
0
Perfectoid ring extends Tate ring

#59 jcommelin opened 4 years ago
0
Local ring homs for stalk maps of CLVRS

#58 jcommelin closed 4 years ago
0
Cleaning up adic_space.lean

#57 jcommelin closed 4 years ago
0
(Q_p, Z_p) is a Huber pair, and Spa(Q_p, Z_p) a singleton

#56 jcommelin closed 4 years ago
0
Padics form a Huber ring

#55 jcommelin closed 4 years ago
0
Group with zero

#54 jcommelin closed 4 years ago
0
Refactor localizations of valuations

#53 jcommelin closed 4 years ago
0
Bump mathlib2

#52 jcommelin closed 4 years ago
0
Bump mathlib

#51 jcommelin closed 5 years ago
0
Fix link, plus more unexpected changes

#50 jcommelin closed 5 years ago
0
linkfix

#49 fpvandoorn closed 5 years ago
2
Some notation tricks to beautify perfectoid-space.lean

#48 PatrickMassot closed 5 years ago
0
Use a parameter for the prime p

#47 jcommelin closed 5 years ago
0
Get rid of nat.Prime

#46 PatrickMassot closed 5 years ago
0
Small start on docs

#45 jcommelin closed 5 years ago
0
Bump mathlib

#44 jcommelin closed 5 years ago
0
Remove for_mathlib/finset.lean -- result exists in mathlib

#43 jcommelin closed 5 years ago
0
Subgroup inter -- don't merge this, `update-mathlib` is lagging

#42 jcommelin closed 5 years ago
0
File not used in project

#41 jcommelin closed 5 years ago
4
preorder.lift -- Merge this after bumping mathlib

#40 jcommelin closed 5 years ago
0
File is not used in project

#39 jcommelin closed 5 years ago
0
This seems to be in mathlib already

#38 jcommelin closed 5 years ago
0
Removing for_mathlib/is_cover.lean; contents are not used

#37 jcommelin closed 5 years ago
0
Remove for_mathlib/subtype.lean; contents are in mathlib

#36 jcommelin closed 5 years ago
0
Wrong category instance for CLVRS

#35 jcommelin closed 5 years ago
1
refactor(perfectoid_space): beautification

#34 jcommelin closed 5 years ago
0
Examples of perfectoid spaces

#33 kbuzzard opened 5 years ago
10
Maths perfectoid space = Lean perfectoid space

#32 kbuzzard opened 5 years ago
0
Documentation

#31 kbuzzard opened 5 years ago
4
Project does not currently compile

#30 kbuzzard closed 5 years ago
2
Topology on A(T/s)

#29 jcommelin closed 5 years ago
0
valuation API

#28 kbuzzard closed 5 years ago
2
limits and colimits of rings and topological rings

#27 kbuzzard closed 5 years ago
0
Adic spaces and perfectoid spaces

#26 kbuzzard closed 5 years ago
0
Constructing the presheaf on Spa(A)

#25 kbuzzard closed 5 years ago
0
Completion of a topological ring

#24 kbuzzard closed 5 years ago
2
Integral closure of a subring

#23 kbuzzard closed 5 years ago
0
Valuation fixes

#22 jcommelin closed 5 years ago
0
Rewrite valuations

#21 jcommelin closed 5 years ago
0
Cleanup notation, unlock rational_open_is_open

#20 jcommelin closed 5 years ago
0