map_neg_eq_conj

Mathlib.Analysis.RCLike.Basic

URI: https://scilib.ai/kg/mathlib#AddChar.map_neg_eq_conj

English

If G is abelian and ψ: G → K is an additive character, then ψ(−x) = conj(ψ(x)) for all x ∈ G.

Русский

Пусть G абелева, иψ: G → K — аддитивный символ. Тогда ψ(−x) = conj(ψ(x)) для всех x ∈ G.

LaTeX

$$$ \\psi(-x) = \\overline{\\psi(x)} $$$

Lean4

theorem map_neg_eq_conj [AddCommGroup G] (ψ : AddChar G K) (x : G) : ψ (-x) = conj (ψ x) := by
  rw [map_neg_eq_inv, inv_apply_eq_conj]

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

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

Разделы

Аффилиация

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