mathlib4-dependent-issues-bot

Results 59 comments of mathlib4-dependent-issues-bot

feat(CategoryTheory/SmallObject/Iteration): the unique morphism (bot and succ cases)

This PR/issue depends on: * ~~leanprover-community/mathlib4#18115~~ By **[Dependent Issues](https://github.com/z0al/dependent-issues)** (🤖). Happy coding!

feat(Algebra/Category/ModuleCat/Presheaf): presheaves of modules are generated by their sections

This PR/issue depends on: * ~~leanprover-community/mathlib4#18159~~ By **[Dependent Issues](https://github.com/z0al/dependent-issues)** (🤖). Happy coding!

feat(Topology/Algebra/Valued/LocallyCompact): locally compact nonarchimedean field iff complete and DVR and finite field

This PR/issue depends on: * ~~leanprover-community/mathlib4#16731~~ * ~~leanprover-community/mathlib4#15777~~ * ~~leanprover-community/mathlib4#16619~~ * ~~leanprover-community/mathlib4#15424~~ * ~~leanprover-community/mathlib4#20373~~ By **[Dependent Issues](https://github.com/z0al/dependent-issues)** (🤖). Happy coding!

refactor(CategoryTheory/Monoidal): typeclasses Functor.LaxMonoidal, Functor.OplaxMonoidal and Functor.Monoidal

This PR/issue depends on: * ~~leanprover-community/mathlib4#17761~~ By **[Dependent Issues](https://github.com/z0al/dependent-issues)** (🤖). Happy coding!

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

This PR/issue depends on: * ~~leanprover-community/mathlib4#18092~~ * ~~leanprover-community/mathlib4#18094~~ * ~~leanprover-community/mathlib4#18096~~ * ~~leanprover-community/mathlib4#18278~~ By **[Dependent Issues](https://github.com/z0al/dependent-issues)** (🤖). Happy coding!

feat: Hoeffding's lemma

This PR/issue depends on: * ~~leanprover-community/mathlib4#20151~~ By **[Dependent Issues](https://github.com/z0al/dependent-issues)** (🤖). Happy coding!

feat(CategoryTheory/SmallObject/Iteration): the unique morphism (limit case)

This PR/issue depends on: * ~~leanprover-community/mathlib4#18115~~ * ~~leanprover-community/mathlib4#18127~~ By **[Dependent Issues](https://github.com/z0al/dependent-issues)** (🤖). Happy coding!

feat(Data/Multiset/Order): add Dershowitz-Manna Ordering and Theorem

This PR/issue depends on: * ~~leanprover-community/mathlib4#15645~~ By **[Dependent Issues](https://github.com/z0al/dependent-issues)** (🤖). Happy coding!

feat(SetTheory/ZFC/Ordinal): von Neumann hierarchy of sets

This PR/issue depends on: * ~~leanprover-community/mathlib4#16996~~ * ~~leanprover-community/mathlib4#17016~~ * ~~leanprover-community/mathlib4#17026~~ * ~~leanprover-community/mathlib4#18239~~ * ~~leanprover-community/mathlib4#19946~~ * ~~leanprover-community/mathlib4#19967~~ By **[Dependent Issues](https://github.com/z0al/dependent-issues)** (🤖). Happy coding!

feat(Algebra/Category/ModuleCat/Presheaf): the endofunctor of presheaves of modules induced by an oplax natural transformation

This PR/issue depends on: * ~~leanprover-community/mathlib4#18197~~ By **[Dependent Issues](https://github.com/z0al/dependent-issues)** (🤖). Happy coding!