Yaël Dillies

feat(analysis/seminorm): Group seminorms

1

Multiplicativize the existing `add_group_seminorm` material. --- [](https://gitpod.io/from-referrer/)

refactor(data/finset/fin): Delete `finset.fin_range`

11

`finset.fin_range n` is just `finset.univ`, so we inline its definition in the `fintype (fin n)` instance to avoid people trying to use it. --- [](https://gitpod.io/from-referrer/)

feat(category_theory/category/Pointed): `Pointed` is a monoidal category

1

Provide the `monoidal_category` and `symmetric_category` instances for `Pointed`. --- This is mostly an exercise for me to see whether I understand monoidal categories. Please suggest missing API. I tried to...

feat(combinatorics/additive/ruzsa_szemeredi): The Ruzsa-Szemerédi problem

2

Prove the (implicit) lower bound on the Ruzsa-Szemerédi problem. --- We can prove the explicit bound once #15327 is merged. Bhavik told me to golf the proof using https://github.com/leanprover-community/mathlib/blob/1874b7ab2089c2c9922e89026527b9806f2d0953/src/combinatorics/szemeredi/triangle.lean#L349-L365 but...

Change the behavior of the infoview to visually distinguish: * frozen instances * typeclass assumptions that are not instances * unfrozen typeclass assumptions * non typeclass assumptions --- The style...

feat(analysis/normed/group/basic): Multiplicative, noncommutative normed groups

1

Define * `seminormed_group` * `seminormed_add_group` * `seminormed_comm_group` * `normed_group` * `normed_add_group` * `normed_comm_group` Additivize all lemmas in `analysis.normed.group.basic`. To disambiguate names, I add one or two `'` to the multiplicative...

refactor(data/int/cast): Use hom classes

6

Restate lemmas using `monoid_with_zero_hom_class`/`ring_hom_class` instead of `monoid_with_zero_hom`/`ring_hom`. --- - [ ] depends on: #15985 [](https://gitpod.io/from-referrer/)

Define `pfun.prod : (α →. γ) → (β →. δ) → α × β →. γ × δ`. --- [](https://gitpod.io/from-referrer/)

chore(*): Rename `is_scalar_tower` to `smul_assoc_class`

1

to match `smul_comm_class` and `vadd_assoc_class`. --- [Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/left.20vs.20right.20modules.20in.20tensor.20products/near/261974400), [other Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/smul_assoc_class) [](https://gitpod.io/from-referrer/)

chore(combinatorics/*): Fix lint

4

Fix the linting errors coming from `fintype_finite`, `to_additive_doc` and `doc_blame`. Pull out a `[projective_plane P L]` assumption to a `variables` declaration in `combinatorics.configuration`. --- [](https://gitpod.io/from-referrer/)