one_right

Mathlib.Algebra.Group.Semiconj.Defs

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

← MathLib Explorer

English

Any element semiconjugates 1 to 1.

Русский

Любой элемент полусопряжает 1 к 1.

LaTeX

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

Lean4

/-- Any element semiconjugates `1` to `1`. -/
@[to_additive (attr := simp) /-- Any element semiconjugates `0` to `0`. -/
    ]
theorem one_right (a : M) : SemiconjBy a 1 1 := by rw [SemiconjBy, mul_one, one_mul]

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

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

Разделы

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

Аффилиация

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