mathlib

mathlib copied to clipboard

https://en.wikipedia.org/wiki/Linear_programming

jcommelin

We will need the Hasse invariant. But let's specialize to Q_p, because we won't have Brauer groups for the time being. https://en.wikipedia.org/wiki/Hasse_invariant_of_a_quadratic_form

jcommelin

Tactic to transfer theorems / definitions using an equivalence.

9

It would be nice to have a tactic that can transfer definitions and / or theorems through equivalences. E.g., all theorems in the upper half of `data/equiv/algebra` should be `by...

urkud

transporting definitions and theorems along isomorphisms.

25

There's a construction called `Spec` which eats a commutative ring `R` and spits out a topological space `Spec R`. To a mathematician it is trivially true that if we have...

kbuzzard

Merge 3 files about basic properties of relations

3

We have at least 3 files with basic facts about relations. * [`data/rel`](https://github.com/leanprover-community/mathlib/blob/master/src/data/rel.lean) defines https://github.com/leanprover-community/mathlib/blob/708faa9f3dba94a57e26ebd27a87cc6cd77a4d06/src/data/rel.lean#L12 then defines (pre)image, (co)domain, composition etc. * [`logic/relation`](https://github.com/leanprover-community/mathlib/blob/master/src/logic/relation.lean) works with `α → β → Prop`...

urkud

Etale cohomology

2

Schemes are ticking along nicely, as is commutative algebra. Currently we still don't have schemes in mathlib, or etale maps of rings, but it is not hard to imagine them...

kbuzzard

It would be nice if someone who understands the exact meaning of all these (greek letter)-expansion will briefly describe the meaning of these suffixes in `docs/contribute/naming.md` for those who (like...

urkud

Currently we have various functions like `complete_lattice.copy` in `order/filter/basic` and `emetric_space.replace_uniformity` in `topology/metric_space/emetric_space`. I think that these functions should be generalized to a tactic (`copy_struct`?) that does the following: 1....

urkud

Probably `setup_tactic_parser` can be integrated to use `open_locale` instead

4

khoek

To do: * [ ] Add some documentation about, like, what a formal roadmap is supposed to be and how people should interact with them. Right now it's a directory...

jcommelin