mulOption_neg_neg — Mathlib

English

Every left option of x*y of the first kind is also a left option of x*(-(-y)) of the first kind, via a negation mapping.

Русский

Каждая левая опция x·y первого вида также является левой опцией x·(-(-y)) первого вида через соответствующее отображение отрицания.

LaTeX

$$mulOption\ x\ y\ i\ j = mulOption\ x\ (-(-y))\ i\ (toLeftMovesNeg\ (toRightMovesNeg\ j))$$

Lean4

/-- Any left option of `x * y` of the first kind is also a left option of `x * -(-y)` of
  the first kind. -/
theorem mulOption_neg_neg {x} (y) {i j} :
    mulOption x y i j = mulOption x (-(-y)) i (toLeftMovesNeg <| toRightMovesNeg j) := by simp [mulOption]

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