neg_right

Mathlib.Algebra.Ring.Semiconj

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

English

If SemiconjBy a x y holds, then SemiconjBy a (−x) (−y) also holds.

Русский

Если SemiconjBy a x y выполняется, то SemiconjBy a (−x) (−y) также выполняется.

LaTeX

$$$\text{SemiconjBy}(a, -x, -y)$$$

Lean4

theorem neg_right (h : SemiconjBy a x y) : SemiconjBy a (-x) (-y) := by simp only [SemiconjBy, h.eq, neg_mul, mul_neg]

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

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

Разделы

Аффилиация

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