add_right — Mathlib

English

If SemiconjBy a x y and SemiconjBy a x' y', then SemiconjBy a (x+x') (y+y').

Русский

Если SemiconjBy a x y и SemiconjBy a x' y', то SemiconjBy a (x+x') (y+y').

LaTeX

$$$ (SemiconjBy a x y) \land (SemiconjBy a x' y') \Rightarrow SemiconjBy a (x+x') (y+y') $$$

Lean4

@[simp]
theorem add_right [Distrib R] {a x y x' y' : R} (h : SemiconjBy a x y) (h' : SemiconjBy a x' y') :
    SemiconjBy a (x + x') (y + y') := by simp only [SemiconjBy, left_distrib, right_distrib, h.eq, h'.eq]

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