Theorem DirichletCharacter.mul_def

Modification history

2023-12-06 12:08
Mathlib/NumberTheory/DirichletCharacter/Basic.lean
feat: mul for DirichletCharacter (#8770) …
Added DirichletCharacter.mul_defView on Github →