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 13 forks source link

Valuation fixes #22

Closed jcommelin closed 5 years ago

jcommelin commented 5 years ago

Sorry, if forgot to fix these little bugs in the previous PR. Note that the file valuation_universes is now merged into the other files. So I deleted it.