mulEquiv_units — Mathlib

English

There is a nonempty multiplicative equivalence between Dirichlet characters mod n and units of ZMod n, under suitable hypotheses on the ring R (enough roots of unity).

Русский

Существует ненулевое умножающееся эквивалентное отображение между символами Дирихле модуля n и единицами ZMod n при подходящих условиях на кольцо R (достаточно корней единицы).

LaTeX

$$$\\text{mulEquiv\\_units}: \\text{Nonempty}(\\text{DirichletCharacter }(R,n) \\simeq\\* (\\mathbb{Z}/n\\mathbb{Z})^{\\times}).$$$

Lean4

/-- The group of Dirichlet characters mod `n` with values in a ring `R` that has enough
roots of unity is (noncanonically) isomorphic to `(ZMod n)ˣ`. -/
theorem mulEquiv_units : Nonempty (DirichletCharacter R n ≃* (ZMod n)ˣ) :=
  MulChar.mulEquiv_units ..

Похожие утверждения