coe_one

Mathlib.Algebra.Group.AddChar

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

English

The unit additive character is the constant-1 function on A.

Русский

Единичный аддитивный характер является константной функцией, отображающей каждый элемент A в единицу in M.

LaTeX

$$$$ \forall a \in A,\; (1 : \mathrm{AddChar}\ A\ M)(a) = 1. $$$$

Lean4

@[simp, norm_cast]
theorem coe_one : ⇑(1 : AddChar A M) = 1 :=
  rfl

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

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

Разделы

Аффилиация

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