zmodAddEquiv_apply — Mathlib

English

There is a bijection between ZMod n and the group of additive characters AddChar (ZMod n) Complex given by zmodAddEquiv.

Русский

Существует биекция между ZMod n и группой аддитивных комплекснозначных символов AddChar (ZMod n) Complex, заданная zmodAddEquiv.

LaTeX

$$$ zmodAddEquiv : ZMod n \simeq_+ AddChar (ZMod n) Complex $$$

Lean4

@[simp]
theorem zmodAddEquiv_apply (x : ZMod n) : zmodAddEquiv x = circleEquivComplex (zmod n x) :=
  rfl

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