fintype — Mathlib

English

There is a finite type structure on DirichletCharacter R n; the set of Dirichlet characters mod n with values in a ring R is finite.

Русский

Существует конечный множество символов Дирихле модуля n с значениями в кольце R; множество таких символов конечно.

LaTeX

$$$\\text{Fintype\\ DirichletCharacter }(R,n)$.$$

Lean4

noncomputable instance fintype {R : Type*} [CommRing R] [IsDomain R] {n : ℕ} : Fintype (DirichletCharacter R n) :=
  .ofFinite _

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