mathlib-dependent-issues-bot

Results 94 comments of mathlib-dependent-issues-bot

feat(category_theory/abelian/transfer): adjoint functor transfers "enough-injectiveness"

This PR/issue depends on: * ~~leanprover-community/mathlib#14581~~ * ~~leanprover-community/mathlib#15262~~ By **[Dependent Issues](https://github.com/z0al/dependent-issues)** (šŸ¤–). Happy coding!

feat(analysis/normed_space/category/CStarAlg): categories of Cā‹†-algebras

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

feat(analysis/calculus/cont_diff): Prove that `fderiv_within` is `C^n` for functions with parameters

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

feat(linear_algebra/matrix): triangular matrices

This PR/issue depends on: * ~~leanprover-community/mathlib#14035~~ * ~~leanprover-community/mathlib#16150~~ By **[Dependent Issues](https://github.com/z0al/dependent-issues)** (šŸ¤–). Happy coding!

chore(analysis/inner_product_space/basic): remove `bilin_form_of_real_inner`

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

feat(analysis/inner_product_space/cross_product): general construction of the cross-product

This PR/issue depends on: * ~~leanprover-community/mathlib#16475~~ * ~~leanprover-community/mathlib#16476~~ * ~~leanprover-community/mathlib#16477~~ * ~~leanprover-community/mathlib#16478~~ * ~~leanprover-community/mathlib#16479~~ * ~~leanprover-community/mathlib#16487~~ By **[Dependent Issues](https://github.com/z0al/dependent-issues)** (šŸ¤–). Happy coding!

feat(analysis/inner_product_space/two_dim): volume/area form of negated orientation

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

feat(analysis/normed_space/hahn_banach/separation): generalize to (locally convex) topological vector spaces

This PR/issue depends on: * ~~leanprover-community/mathlib#16782~~ * ~~leanprover-community/mathlib#16749~~ By **[Dependent Issues](https://github.com/z0al/dependent-issues)** (šŸ¤–). Happy coding!

chore(algebra/order/monoid_lemmas_zero_lt): move all positivity assumptions to the first place

This PR/issue depends on: * ~~leanprover-community/mathlib#16172~~ * ~~leanprover-community/mathlib#16189~~ By **[Dependent Issues](https://github.com/z0al/dependent-issues)** (šŸ¤–). Happy coding!

feat(topology/homotopy/homotopy_group): `group` and `comm_group` instances for `Ļ€_n`

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