Open kbuzzard opened 5 years ago
The list of files (sorted, somehow) that is not in for_mathlib/
:
Huber_ring/basic.lean
Huber_ring/localization.lean
Huber_ring/padics.lean
Spa/localization_Huber.lean
Spa/rat_open_data_completion.lean
Spa/space.lean
Spa/stalk_valuation.lean
examples/empty.lean
examples/padics.lean
valuation/basic.lean
valuation/canonical.lean
valuation/field.lean
valuation/group_with_zero.lean
valuation/linear_ordered_comm_group_with_zero.lean
valuation/localization.lean
valuation/topology.lean
valuation/valuation_field_completion.lean
valuation/with_zero_topology.lean
Frobenius.lean
Huber_pair.lean
Tate_ring.lean
adic_space.lean
continuous_valuations.lean
perfectoid_space.lean
power_bounded.lean
valuation_spectrum.lean
For the files that are not in sheaves/
or for_mathlib
:
There is still a list of TODO's, and things can be quite improved. But this list seems to have served it's purpose.
Thanks for your amazing efforts with this list Johan!
I didn't close this on purpose, because Kevin's first post contains a bunch of stuff that hasn't been done yet. (Even though, it's not likely that we'll get to it soon.)
The code should somehow be documented. My dream for this would be that the low-level files (like
valuation.basic
) just get big comment blocks at the top explaining the API of the file, and the higher level files get LaTeX code which could be read using Patrick's formatter. I am a bit unclear about what exactly we can do here, but ultimately now we have the code I think that we should be thinking about trying to make what we have more accessible to mathematicians.