mathlib-dependent-issues-bot

Results 94 comments of mathlib-dependent-issues-bot

feat(category_theory/limits): has_limits_of_shape J if and only if const J is a left adjoint

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

feat(representation_theory/character): orthogonality of characters

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

feat(topology/uniform_space/uniform_convergence_topology): continuity of [pre,post]composition, and other topological properties

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

feat(topology/algebra/uniform_ring): ring completions and algebra structures

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

feat(number_theory/geometry_of_numbers): Blichfeldt and Minkowski's theorems

This PR/issue depends on: * ~~leanprover-community/mathlib#8591~~ * ~~leanprover-community/mathlib#8600~~ * ~~leanprover-community/mathlib#8608~~ * ~~leanprover-community/mathlib#8695~~ * ~~leanprover-community/mathlib#16708~~ * leanprover-community/mathlib#17030 By **[Dependent Issues](https://github.com/z0al/dependent-issues)** (🤖). Happy coding!

feat(linear_algebra/projective_space/subspace): adds constructors for projective subspaces

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

feat(analysis/locally_convex/barrel): barreled spaces

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

feat(analysis/convolution): prove associativity under more convenient assumptions

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

feat(analysis/complex/open_mapping): the open mapping thm for holomorphic functions

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

refactor(algebraic_geometry/projective_spectrum/topology): refactor projective_spectrum def into structure

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