mathlib

mathlib copied to clipboard

Expand the surreals library

3

We currently have a definition of the [surreal numbers](https://en.wikipedia.org/wiki/Surreal_number) in [surreal.lean](https://github.com/leanprover-community/mathlib/blob/master/src/set_theory/surreal.lean), but there is still more to be done here. The next steps would be to show that the arithmetic...

rwbarton

assoc_rw can leave side-goals as metavariables

1

e.g. ```lean import group_theory.basic example {G : Type*} [add_comm_group G] (h : ∀ (g :G) (t : g ≠ 0), g + g =0) (g f : G): f +...

alexjbest

Geometric Algebra

4

According to Prof. Alan Macdonald's [page](http://www.faculty.luther.edu/~macdonal/) GA: >... and its extension to geometric calculus unify, simplify, and generalize vast areas of mathematics that involve geometric ideas, including linear algebra, multivariable...

jfcg

There are still probably things that can be done to improve the `number_theory/padic_norm.lean`. Some ideas: - [x] Split the file in two at the definition `padic_norm` with that latter part...

BoltonBailey

The `deprecated/` folder is no longer imported by mathlib. However there is something worth salvaging: the `is_monoid_hom` class, and all its relatives, could be converted to structures and moved back...

kim-em

`to_` framework

1

`to_additive` has had great success in homogenizing lemmas and reducing maintenance burden. It would now be great to extend this principle to other kinds of dualities: * `to_add_op`: Turn lemmas...

YaelDillies

squeeze_simp also simplify targets

3

Currently `squeeze_simp [blah] at *` reduces the list of lemmas applied to only those that are actually applied, but still applies to all hypotheses and the goal. It would be...

alexjbest

TODO: unify `disjoint`

7

Introduce `disjoint` on `has_mem` and unify the `list`, `multiset`, `finset` instances. The `finset` instance would be generalized by removing the requirement for `decidable_eq`

johoelzl

Unify (or at least connect) `order_hom` and `rel_hom`

1

`order_hom` is essentially the same as a `rel_hom` between two instances of `≤`. One of two things should happen: - `order_hom` should be refactored to be based on `rel_hom`, with...

awainverse

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

jcommelin