search

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

Some notation tricks to beautify perfectoid-space.lean #48

Closed PatrickMassot closed 5 years ago

PatrickMassot commented 5 years ago

We discussed this on Zulip, but without a really clear conclusion, so I'll let you decide while I sleep.