outsidePart_add — Mathlib

English

If p ≠ 0, then (p+q).outsidePart = p.outsidePart + q.

Русский

Если p ≠ 0, тогда (p+q).outsidePart = p.outsidePart + q.

LaTeX

$$$$ p \neq 0 \implies (p+q).outsidePart = p.outsidePart + q. $$$$

Lean4

@[simp]
theorem outsidePart_add : (p + q).outsidePart = p.outsidePart + q :=
  by
  simp_rw [outsidePart, firstReturn_add, add_eq_zero', h, false_and, dite_false, ite_false, DyckWord.ext_iff, drop]
  exact drop_append_of_le_length (firstReturn_lt_length h)

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