sub_right — Mathlib

English

In a nonunital nonassoc ring, subtraction on the right distributes over semiconjugacy: h.sub_right h'.

Русский

В кольце без единицы и без ассоциаций вычитание справа распределяет SemiconjBy: h.sub_right h'.

LaTeX

$$$\text{SubRight}(h,h')$$$

Lean4

@[simp]
theorem sub_right (h : SemiconjBy a x y) (h' : SemiconjBy a x' y') : SemiconjBy a (x - x') (y - y') := by
  simpa only [sub_eq_add_neg] using h.add_right h'.neg_right

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