mathlib-dependent-issues-bot

Results 94 comments of mathlib-dependent-issues-bot

feat(probability/independence): Kolmogorov's 0-1 law

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

feat(topology/algebra/module/strong_operator, analysis/normed_space/operator_norm): strong operator topology

This PR/issue depends on: * ~~leanprover-community/mathlib#14857~~ * ~~leanprover-community/mathlib#16052~~ * ~~leanprover-community/mathlib#16054~~ 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(geometry/euclidean/ceva) : Ceva's Theorem, problem 61 on Freek's list

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

feat(combinatorics/additive/ruzsa_szemeredi): The Ruzsa-Szemerédi problem

This PR/issue depends on: * ~~leanprover-community/mathlib#19202~~ * ~~leanprover-community/mathlib#19203~~ 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!

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!

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

docs(tutorials/representation_theory): beginnings of a tutorial following Etingof's notes

This PR/issue depends on: * ~~leanprover-community/mathlib#13908~~ * ~~leanprover-community/mathlib#13905~~ * ~~leanprover-community/mathlib#13882~~ * ~~leanprover-community/mathlib#13933~~ * ~~leanprover-community/mathlib#13934~~ * ~~leanprover-community/mathlib#13961~~ * ~~leanprover-community/mathlib#14023~~ 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~~ * ~~leanprover-community/mathlib#17535~~ * ~~leanprover-community/mathlib#17536~~ * ~~leanprover-community/mathlib#17590~~ * ~~leanprover-community/mathlib#17766~~ * ~~leanprover-community/mathlib#17771~~ * ~~leanprover-community/mathlib#17773~~ * ~~leanprover-community/mathlib#17774~~...