map_add_eq_mul

Mathlib.Algebra.Group.AddChar

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

← MathLib Explorer

English

An additive character turns sums into products: χ(x+y)=χ(x)χ(y).

Русский

Аддитивный характер превращает сложение в умножение: χ(x+y)=χ(x)χ(y).

LaTeX

$$$\psi(x+y)=\psi(x)\psi(y)$$$

Lean4

/-- An additive character maps sums to products. -/
theorem map_add_eq_mul (ψ : AddChar A M) (x y : A) : ψ (x + y) = ψ x * ψ y :=
  ψ.map_add_eq_mul' x y

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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