one_left

Mathlib.Algebra.Group.Semiconj.Defs

URI: https://scilib.ai/kg/mathlib#SemiconjBy.one_left

← MathLib Explorer

English

The unit 1 semiconjugates any element to itself.

Русский

Единица полусопрягает любое значение к самому себе.

LaTeX

$$$$\forall x\in M:\ SemiconjBy\ 1\ x\ x.$$$$

Lean4

/-- One semiconjugates any element to itself. -/
@[to_additive (attr := simp) /-- Zero semiconjugates any element to itself. -/
    ]
theorem one_left (x : M) : SemiconjBy 1 x x :=
  Eq.symm <| one_right x

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

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

Разделы

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

Аффилиация

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