mathlib4

mathlib4 copied to clipboard

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

erdOne

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

erdOne

--- Preliminary to removing the order dependency from `Mathlib/Data/Nat/Defs.lean`, but that needs a little more work [](https://gitpod.io/from-referrer/)

Ruben-VandeVelde

A semisimple Lie algebra is a direct sum of simple Lie algebras

4

In characteristic zero, a [semisimple Lie algebra](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Lie/Semisimple.html#LieAlgebra.IsSemisimple) is a direct sum of [simple Lie algebra](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Lie/Semisimple.html#LieAlgebra.IsSimple)s. We should add this result to Mathlib. I think the most useful statement of this...

ocfnash

Lean pr testing 4272

4

testing more aggressive caching --- [](https://gitpod.io/from-referrer/)

JovanGerb

feat (NumberTheory/Harmonic): compute Gamma'(1/2)

3

Show `Gamma'(1/2) = -√π * (γ + 2 * log 2)` and various other related results. --- [](https://gitpod.io/from-referrer/)

loefflerd

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

Komyyy

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

Ruben-VandeVelde

feat: morphisms of presheaves that are locally injective for a Grothendieck topology

1

This PR creates the file `CategoryTheory.Sites.LocallyInjective` which develops the basic API of locally injective morphisms of presheaves. The file `CategoryTheory.Sites.Surjective` is renamed `CategoryTheory.Sites.LocallySurjective` and shall be expanded in a future...

joelriou

feat(CategoryTheory): right derived functors

1

In this PR, given a functor `F : C ⥤ H`, and `L : C ⥤ D` that is a localization functor for `W : MorphismProperty C`, we define `F.totalRightDerived...

joelriou