Johan Commelin

properties of (sub)modules

1

- [x] finite - [x] finitely generated (done for submodules, we might want a wrapper to make life easier when working with a full module) (#4634) - [ ] finitely...

remove the coercion from zmod n to other rings

1

We should remove the coercion, and just use `zmod.cast(_hom)` everywhere. The coercion causes more trouble than it is worth. This coercion is currently used in evil ways, by coercing from...

wlog

4

It is nontrivial (currently for me impossible) to use `wlog` in the following example. ```lean lemma forty_two (a b c : ℕ) (h : (0:ℚ) < 1 - (1/a +...

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

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

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...

--- [](https://gitpod.io/from-referrer/)