Scott Carnahan

icon company U. Tsukuba icon location Main activity: Moonshine, vertex algebras, inf. dim. Lie algebras, algebraic geometry.

Results 5 comments of Scott Carnahan

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

Thank you for the review! bors r+

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

@alreadydone suggested marking the definition of `of` reducible. I tried it, and it had the following effects: 1. all `@[simp]` lemmas with `of` in the statement made the simpNF linter...

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

bors r+

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

bors r+

feat(RingTheory/LaurentSeries): add properties of the X-adic valuation on Laurent series

Have you considered using `AddVal` from `Mathlib.RingTheory.HahnSeries.Summable`? It looks like the `order` API from Hahn series can make some of your proofs shorter.