one_eq_zero

Mathlib.Algebra.Group.AddChar

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

English

In this additive-character structure, the unit and the zero elements coincide: 1 = 0.

Русский

В этой структуре аддитивных характеров единица и ноль совпадают: 1 = 0.

LaTeX

$$$$ (1 : \mathrm{AddChar}\ A\ M) = (0 : \mathrm{AddChar}\ A\ M). $$$$

Lean4

theorem one_eq_zero : (1 : AddChar A M) = (0 : AddChar A M) :=
  rfl

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

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

Разделы

Аффилиация

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