instUniqueOfNatNat

Mathlib.NumberTheory.DirichletCharacter.Basic

URI: https://scilib.ai/kg/mathlib#DirichletCharacter.instUniqueOfNatNat

English

For any commutative monoid with zero R, there exists a unique Dirichlet character of modulus 1.

Русский

Для любого коммутативного моноида с нулём R существует единственный символ Дирихле модуля 1.

LaTeX

$$$\\exists! \\chi \\in \\mathrm{DirichletCharacter}(R,1).$$$

Lean4

noncomputable instance : Unique (DirichletCharacter R 1) :=
  Unique.mk' (DirichletCharacter R 1)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru