Yaël Dillies
Yaël Dillies
Multiplicativize the existing `add_group_seminorm` material. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)
`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. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)
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...
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...
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...
Restate lemmas using `monoid_with_zero_hom_class`/`ring_hom_class` instead of `monoid_with_zero_hom`/`ring_hom`. --- - [ ] depends on: #15985 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)
Define `pfun.prod : (α →. γ) → (β →. δ) → α × β →. γ × δ`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)
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) [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)
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`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)