Mitchell Lee

feat: completion of a uniform multiplicative group

4

Multiplicativize `Topology.Algebra.GroupCompletion`. That is, rewrite it in the multiplicative setting and recover the original results using `@[to_additive]`. - Because `@[to_additive]` doesn't work with `noncomputable section` (https://github.com/leanprover/lean4/pull/2610), some instances with `@[to_additive]`...

Prove the following. - `Inducing.hasProd_iff` / `Inducing.hasSum_iff`: Let $g \colon \beta \to \alpha$ be an inducing homomorphism of topological additive commutative monoids. A series $\sum_{i \in I} b_i$ unconditionally converges...

feat: the equational criterion for flatness

5

We prove the [equational criterion for flatness](https://stacks.math.columbia.edu/tag/00HK). As a consequence, every homomorphism from a finitely presented module to a flat module factors through a finite free module. --- - [x]...

feat: the standard geometric representation of a Coxeter group

1

We define the standard geometric representation of a Coxeter group and prove that it is faithful. --- - [ ] depends on: #11526 [](https://gitpod.io/from-referrer/)

feat: the Chebyshev polynomials C and S

2

We define the rescaled Chebyshev polynomials $C_n$ and $S_n$ (also known as the Vieta–Lucas and Vieta–Fibonacci polynomials, respectively). They are related to the Chebyshev polynomials $T_n$ and $U_n$ by the...

feat: index Chebyshev polynomials by integers instead of natural numbers

3

--- [](https://gitpod.io/from-referrer/)

feat: multiple universe polymorphism for the equational criterion for flatness

1

`Algebra/Module/FinitePresentation.lean` is now fully universe polymorphic. This had the side effect of somehow breaking `RingTheory/Flat/EquationalCriterion.lean`, even though I didn't even touch that file. Should I even be trying to do...