Mitchell Lee

feat: Infinite products

1

Last year, YaelDillies made a pull request to mathlib3 that unfortunately never got merged in: https://github.com/leanprover-community/mathlib/pull/18405. This is the mathlib4 version of that pull request. We define arbitrarily indexed products...

feat: the root space of a Coxeter group and the bilinear form on it

11

Prepare to define the standard geometric representation of a Coxeter group by defining the root space and the bilinear form on it. Then prove some lemmas about the orthogonal reflections...

feat: reflections, inversion sequences in Coxeter groups

5

- Add theorem `List.length_eraseIdx_add_one` to `Data/List/Basic.lean`, which states that if `i < l.length`, then the length of `l.eraseIdx i plus one` is equal to the length of `l`. - Add...

feat: add length, reduced words in Coxeter groups

1

Add new file `GroupTheory/Coxeter/Length.lean`. Define the length function and reduced words of Coxeter groups. Prove their basic properties. I decided to split #11408 (now closed) into two pull requests. This...

feat: convergence of infinite sums in nonarchimedean abelian groups

2

Let `G` be a complete nonarchimedean abelian group and let `f : α → G` be a function. We prove that `f` is unconditionally summable if and only if `f...

feat: value of f (x + n * c), where f is antiperiodic with antiperiod c

4

Add `@[simp]` theorem `negOnePow_two_mul_add_one` to `Algebra.GroupPower.NegOnePow`, which states that `(2 * n + 1).negOnePow = -1`. Add theorems to `Algebra.Periodic` about the value of `f (x + n • c)`,...

feat: add simple reflections, words, lifting to Coxeter groups

3

- Move all material about Coxeter groups from GroupTheory/SpecificGroups to GroupTheory/Coxeter. - Slightly change the definition of a Coxeter system so the associated matrix actually needs to be a Coxeter...

feat: completion of a nonarchimedean multiplicative group

1

We prove that the completion of a nonarchimedean multiplicative group is a nonarchimedean multiplicative group. --- - [x] depends on: #12669 - [ ] depends on: #11837 [](https://gitpod.io/from-referrer/)

feat: the product of two sums in a nonarchimedean ring

1

We prove that in a nonarchimedean ring, $$\sum_{(i, j) \in I \times J} a_i b_j = \left(\sum_{i \in I} a_i \right)\left(\sum_{j \in J} b_j\right),$$ provided that both sums on the...

feat: "outer product" of functions that tend to zero on the cocompact filter

3

Let `M` be a topological space with a continuous multiplication operation and a zero. We prove that if `f : α → M` and `g : β → M` are...