birthday_sub — Mathlib

English

The birthday of a subtraction equals the birthday addition: (x - y).birthday = x.birthday.nadd y.birthday.

Русский

Дни рождения вычитания равны естественному суммированию: (x - y).birthday = x.birthday.nadd y.birthday.

LaTeX

$$$ (x - y).birthday = x.birthday.nadd y.birthday $$$

Lean4

@[simp]
theorem birthday_sub (x y : PGame) : (x - y).birthday = x.birthday ♯ y.birthday :=
  by
  apply (birthday_add x _).trans
  rw [birthday_neg]

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