neg_one_right

Mathlib.Algebra.Ring.Semiconj

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

English

For a, the semiconjugacy by a with −1 on the right is immediate: a · (−1) · (−1) defines a semiconjugacy.

Русский

Для любого a выполняется: semiconjBy a (−1) (−1).

LaTeX

$$$\operatorname{SemiconjBy}(a, -1, -1)$$$

Lean4

theorem neg_one_right (a : R) : SemiconjBy a (-1) (-1) := by simp

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

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

Разделы

Аффилиация

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