add_eq_zero — Mathlib

English

For any x,y, x+y ≡ 0 if and only if x ≡ 0 and y ≡ 0.

Русский

Для любых x,y, x+y эквивалентно 0 тогда и только тогда, когда x ≡ 0 и y ≡ 0.

LaTeX

$$$ (x+y) \equiv 0 \iff (x \equiv 0) \land (y \equiv 0) $$$

Lean4

protected theorem add_eq_zero : ∀ {x y : PGame}, x + y ≡ 0 ↔ x ≡ 0 ∧ y ≡ 0
  | mk xl xr xL xR, mk yl yr yL yR =>
    by
    simp_rw [identical_zero_iff, leftMoves_add, rightMoves_add, isEmpty_sum]
    tauto

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