neg_left

Mathlib.Algebra.Ring.Semiconj

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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