mathlib

mathlib copied to clipboard

feat(set_theory/game/basic): Golf using `antisymmetrization` API

4

--- - [x] depends on: #13963 I wasn't able to redefine `game` as `antisymmetrization pgame (≤)`. For whatever reason, that broke a few instances of the `⟦x⟧` notation. [![Open in...

vihdzp

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

adamtopaz

feat(tactic/recommend): `recommend` tactic based on premise selection

4

The `recommend` tactic searches for lemmas in the current environment that look like they could be useful to prove the current goal. It is based on premise selection heuristic used...

gebner

Define the Jacobson radical of a ring as the intersection of all maximal left ideals, and prove basic properties: famous equivalent conditions for an element in a ring to be...

haruhisa-enomoto

feat(order/filter,topology/instances/nnreal): upgrade some lemmas to `iff`

1

* Add `codisjoint.inf_left_sup_inf_right` and `is_compl.le_inf_sup_inf`. * Add `filter.comap_ite`, `filter.comap_max`, and `filter.tendsto_ite`. * Add `real.map_to_nnreal_at_top`, `real.comap_to_nnreal_at_top`, and `real.tendsto_to_nnreal_at_top_iff`. * Rename `tendsto_real_to_nnreal` to `filter.tendsto.real_to_nnreal` so that it can be used with dot...

urkud

Basics of tempered distributions

1

This is another tracking issue for me, but if anyone is interested in helping out, then I would be very happy. The goal is to get tempered distributions and the...

mcdoll

Arithmetic of quadratic fields

6

Basic arithmetic of quadratic fields (ring of integers, discriminant and so on) should now not be too difficult. [https://en.wikipedia.org/wiki/Quadratic_field](https://en.wikipedia.org/wiki/Quadratic_field) [https://en.wikipedia.org/wiki/Quadratic_integer](https://en.wikipedia.org/wiki/Quadratic_integer)

riccardobrasca

As part of the porting process to Lean 4, we should refactor mathlib to remove occurences of ```lean local attribute [semireducible] foobar attribute [irreducible] xyzzy ``` The following data is...

jcommelin

Prior to #18163, the behavior was to sort based on the repr, meaning, that `{0, 5, 10}` is sorted as `{0, 10, 5}`. After #18163, the order is non-deterministic and...

eric-wieser

Define Banach algebras

2

* [x] Define Banach algebras: it turns out that we already have `normed_algebra`s; * [ ] Prove facts about convergence of series for Banach algebras; * [ ] Migrate some...

urkud