Commit 2023-12-06 12:08 9d4c1284
View on Github →feat: mul for DirichletCharacter (#8770) Multiply Dirichlet characters at a common level and obtain their associated primitive character. It also includes a lemma confirming the primitiveness of the resulting character.