mathlib4

mathlib4 copied to clipboard

feat: target of final functor is connected iff source is connected

3

This PR is part of the effort to prove the Freyd-Mitchell embedding theorem. --- [](https://gitpod.io/from-referrer/)

datokrat

This PR defines the composite of two heterogeneous vertex operators as a heterogeneous vertex operator, using iterated Hahn series. Composite vertex operators appear in some definitions of vertex algebras. Additional...

ScottCarnahan

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

ADedecker

refactor(Algebra/Polynomial/Laurent): use Int.ofNat.inj

6

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

mo271

This seems like a reasonable thing to split out, and it also makes `Associated.lean` not depend on as much order theory. --- [](https://gitpod.io/from-referrer/)

Ruben-VandeVelde

refactor(Topology/Category): unify some definitions of subcategories of compact Hausdorff spaces

2

This PR unifies the definitions of the categories `CompHaus`, `Profinite`, `Stonean`, and `LightProfinite` by defining a structure `CompHausLike P` depending on a predicate `P` on topological spaces. Many of the...

dagurtomas

refactor(Order/JordanHolder): use `RelSeries` to implement `CompositionSeries`

3

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

jjaassoonn

feat: two equiv involving `Associates` and `nonZeroDivisors`

2

This PR contains mainly the following two equivalences: ```lean def nonZeroDivisorsUnitsEquiv (α : Type*) [MonoidWithZero α] : (α⁰)ˣ ≃* αˣ ``` and ```lean def AssociatesNonZeroDivisorsMulEquiv (α : Type*) [CommMonoidWithZero α]...

xroblot

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

StevenClontz

feat: add competely normal (non-Hausdorff) property

2

This conribution adds a distinct notion of a (non-Hausdorff) completely normal space, and disintangles relevant results that do not require Hausdorff. --- [](https://gitpod.io/from-referrer/)

StevenClontz