mulShift_one

Mathlib.Algebra.Group.AddChar

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

English

For any ψ, mulShift ψ 1 = ψ.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem mulShift_one (ψ : AddChar R M) : mulShift ψ 1 = ψ := by ext; rw [mulShift_apply, one_mul]

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

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

Разделы

Аффилиация

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