mathlib4

mathlib4 copied to clipboard

feat(Mathlib/Data/Seq/Seq): prove `∀ a ∈ (s : Seq' α), p a` using coinduction

3

--- - [ ] depends on: #13509 This PR consists [Continued fractions makes an isomorphism between irrationals and baire space ](https://github.com/users/Komyyy/projects/3/) project [](https://gitpod.io/from-referrer/)

Komyyy

feat(Topology/Group): Open normal subgroup in clopen nhds

8

Proving that there is always an open normal subgroup in a clopen nhd of compact topological group Co-authored-by: NailinGuan Yi Song Xuchun Li --- - [x] depends on: #16980 -...

Thmoas-Guan

feat(CategoryTheory/Comma): limit properties of subcategories defined by morphism properties

2

We show that under suitable assumptions on `P` the full subcategory of `Over X` defined by `P` has terminal objects and pullbacks. --- - [x] depends on: #18088 [![Open in...

chrisflav

feat: prove Cauchy's upper bound on polynomial roots

4

--- - [x] depends on: #16582 [](https://gitpod.io/from-referrer/)

Command-Master

feat(CategoryTheory/Grothendieck): `Grothendieck.pre` for Grothendieck construction base change

3

Needed in order to use the Grothendieck construction as a way to express dependent double colimits. This also makes the following changes: * Improves `Grothendieck.comp_base` to trigger without using `erw`...

javra

feat: Hoeffding's lemma

3

Formalize Hoeffding's lemma using the property of cumulant. Co-authored-by: Yuma Mizuno [[email protected]](mailto:[email protected])

tukamilano

refactor: generalize Mul of Submodule and SMul of Ideal on Submodule to noncommutative setting

6

Instead of using `Submodule.map₂` (which doesn't apply in the noncommutative setting), redefine the `Mul` and `SMul` to be defeq to `AddSubmonoid.mul`. In general, if a semiring A is a module...

alreadydone

feat(Topology/Group/Profinite): Profinite group is limit of finite group

2

Prove that any profinite group is limit of finite groups. --- - [ ] depends on: #16976 - [x] depends on: #16980 - [ ] depends on: #16991 [![Open in...

Thmoas-Guan

feat(Bicategory/Functorbicategory): define bicategory of pseudofunctors

3

This PR contains a definition of the bicategory of pseudofunctors, in the file `Bicategory/FunctorBicategory/Pseudo.lean`. It also moves the file `Bicategory/Functorbicategory.lean` to `Bicategory/FunctorBicategory/Oplax.lean`. --- - [x] depends on: #14028 - [...

callesonne

feat(Bicactegory/NaturalTransformation): refactor strong natural transformations

2

This PR is a minor refactor of strong natural transformations. Previously, I had defined strong natural transformations between oplax functors. Now I specialize this directly to pseudofunctors and improve the...

callesonne