Scott Carnahan

feat (RingTheory/Binomial) : Standard lemmas for Ring.choose

2

This PR has basic identities satisfied by general binomial coefficients, together with corresponding lemmas about evaluating Pochhammer polynomials. --- - [ ] depends on: #13428 - [ ] depends on:...

refactor(RingTheory/HahnSeries) : several generalizations

3

This PR is a container for several smaller PRs that refactor and generalize the existing Hahn series theory. It is (I think) all we need from Hahn series to get...

feat (RingTheory/HahnSeries/Multiplication): module structure on HahnModule

4

We add some theorems and instances for Hahn Modules, in particular, a `HahnSeries Γ R`-module structure on `HahnModule Γ R V` for `R` a semiring and `V` an `R`-module. Some...

This PR defines the composite of two heterogeneous vertex operators as a heterogeneous vertex operator, using iterated Hahn series. Composite vertex operators appear in some definitions of vertex algebras. Additional...

feat (RootSystem/Hom): endomorphisms and automorphisms of root pairings

1

This PR introduces the root pairing endomorphism monoid and automorphism group, and shows that the representations on weight and coweight spaces are injective. --- [](https://gitpod.io/from-referrer/)