mulShift_zero

Mathlib.Algebra.Group.AddChar

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

← MathLib Explorer

English

For any ψ, mulShift ψ 0 = 1.

Русский

Пусть ψ — аддитивный характер. Тогда mulShift ψ 0 = 1.

LaTeX

$$$mulShift(ψ, 0) = 1$$$

Lean4

/-- `mulShift ψ 0` is the trivial character. -/
@[simp]
theorem mulShift_zero (ψ : AddChar R M) : mulShift ψ 0 = 1 := by ext;
  rw [mulShift_apply, zero_mul, map_zero_eq_one, one_apply]

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

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

Разделы

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

Аффилиация

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