mathlib4
mathlib4 copied to clipboard
leanprover-community
The math library of Lean 4
Add the Hurwitz zeta function (defined as the sum of its even and odd parts, which were already defined in previous PR's). --- [](https://gitpod.io/from-referrer/)
--- [](https://gitpod.io/from-referrer/)
After being delegated, I forgot to apply the suggestions from #13902 by @jcommelin .... --- [](https://gitpod.io/from-referrer/)
Given a commutative ring `R`, this PR defines the equivalence of categories between `R`-coalgebras and comonoid objects in the category of `R`-modules. We then use this to set up boilerplate...
This PR provides a characterisation of discrete condensed sets and modules, both in the light setting and the classical one. * A condensed module is discrete if and only if...
This is the second part of the refactor of CompHaus and friends (refactoring the definition of `LightProfinite` in terms of `CompHausLike`, see #12930 for the end result) --- - [x]...
This is the second part of the refactor of CompHaus and friends (refactoring the definition of `Stonean` in terms of `CompHausLike`, see #12930 for the end result) --- - [x]...
This is the second part of the refactor of CompHaus and friends (refactoring the definition of `Profinite` in terms of `CompHausLike`, see #12930 for the end result) --- - [x]...
This PR refactors the file `CompHaus.Basic` in terms of the new `CompHausLike` API. Other files are touched only to fix errors created by this refactor, they will be refactored later...
This PR refactors the definition of the right Kan extension functor (`Functor.ran : (C ⥤ E) ⥤ (D ⥤ E)`) which sends a functor to its right Kan extension along...
