Kevin Buzzard
Kevin Buzzard
Theorem: to give a term of type `perfectoid space X` is to give a perfectoid space (in the sense used in the mathematical literature). Proof: Looking at the definition of...
This PR does a couple of things. 1) I remove all irrelevant imports, opens and open-locales. Undocumented and unused commands just confuse the non-expert reader. 2) I write the document...
I've added a lot of comments for the `profinite` example Lean file. My personal opinion from having watched students is that there are two kinds. There are those that don't...
I just finished a level of NNG, and the message at the end said "here's a backwards way of doing this level". So I switched to editor mode to experiment...
Let R be a Dedekind domain with field of fractions K. This PR does two things: 1) makes the finite adeles of K/R into a K-algebra 2) turns `finiteAdeleRing` into...
These instances make it possible to argue with multiplication and inequalities in `ℤₘ₀` . --- [](https://gitpod.io/from-referrer/) These instances are in a bit of a funny place (they need...
`IsDedekindDomain.HeightOneSpectrum.adicCompletion` is currently a `def` and this causes a bunch of `rw`s to fail in Lean 4; `erw` is needed. In developing the API further I ran into more irritating...
Use `SubmodulesRingBasis` to put a topology on the finite adeles. --- Remark: when this work was WIP and depended on other PRs it was #13703 (with no reviewer comments). Now...
Add docstring for `@[reassoc]` attribute. --- [](https://gitpod.io/from-referrer/) Note that, in contrast to when I'm adding maths docstrings, here I know far less about what I'm talking about (in...