English
Let χ1 be a Dirichlet character modulo n and χ2 a Dirichlet character modulo m. There is a Dirichlet character modulo lcm(n,m) obtained by pulling χ1 and χ2 back to the common modulus and multiplying them. This defines a natural product operation on Dirichlet characters at possibly different moduli.
Русский
Пусть χ1 — символы Дирихле модуля n, χ2 — символ Дирихле модуля m. Существует символ Дирихле модуля lcm(n,m), получаемый путём тяготы χ1 и χ2 к общему модулю и перемножения. Это задаёт естественное произведение символов Дирихле различной степени модульности.
LaTeX
$$$\\text{Let } n,m \\in \\mathbb{N},\\; χ_1 \\in \\text{DirichletCharacter}(R,n),\\; χ_2 \\in \\text{DirichletCharacter}(R,m).\\\\\n\\text{Then } χ_1\\mul χ_2 \\in \\text{DirichletCharacter}(R,\\operatorname{lcm}(n,m))\\\\\n\\text{is defined by }(χ_1\\mul χ_2)(a)=χ_1\\bigl(a\\bmod n\\bigr)\\,χ_2\\bigl(a\\bmod m\\bigr),\\text{ for }a \\in (\\mathbb{Z}/\\operatorname{lcm}(n,m)\\mathbb{Z})^{\\times}. $$$
Lean4
/-- Dirichlet character associated to multiplication of Dirichlet characters,
after changing both levels to the same -/
noncomputable def mul {m : ℕ} (χ₁ : DirichletCharacter R n) (χ₂ : DirichletCharacter R m) :
DirichletCharacter R (Nat.lcm n m) :=
changeLevel (Nat.dvd_lcm_left n m) χ₁ * changeLevel (Nat.dvd_lcm_right n m) χ₂
