mathlib-dependent-issues-bot

Results 94 comments of mathlib-dependent-issues-bot

feat(group_theory/index): criterion for subgroups of index two

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

feat(analysis/bounded_variation): functions of bounded variation are ae differentiable

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

feat(topology/metric_space/infsep): Add "infimum separation".

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

feat(topology/algebra/module/basic): a hyperplane is either closed or dense

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

feat(information_theory/linear_code): Define linear codes

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

feat(analysis/normed_space/star/multiplier): construct the multiplier algebra of a C*-algebra

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

refactor(algebra/order/floor): Relax lemmas to remove `linear_order` requirement

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

feat(topology/continuous_function/ideals): maximal ideals correspond to (complements of) singletons

This PR/issue depends on: * ~~leanprover-community/mathlib#16709~~ * ~~leanprover-community/mathlib#16713~~ * ~~leanprover-community/mathlib#16714~~ * ~~leanprover-community/mathlib#16677~~ * ~~leanprover-community/mathlib#16663~~ * ~~leanprover-community/mathlib#16721~~ * ~~leanprover-community/mathlib#16722~~ * ~~leanprover-community/mathlib#16801~~ By **[Dependent Issues](https://github.com/z0al/dependent-issues)** (🤖). Happy coding!

feat(data/nat/choose/multinomial): add multinomial theorem

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

feat(geometry/euclidean/oriented_angle): refactor to a basis-free definition

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~~ * ~~leanprover-community/mathlib#16928~~ * ~~leanprover-community/mathlib#16929~~ * ~~leanprover-community/mathlib#16939~~ By **[Dependent Issues](https://github.com/z0al/dependent-issues)** (🤖). Happy coding!