x_sub_y_dvd_pow_lem — Mathlib

English

For given a, a1, and integers y2,y1,y0,..., a lemma relating a combination of x and y holds; specifically an identity in integers that supports divisibility arguments used later.

Русский

Для данных a и a1 и целых чисел y2,y1,y0,... существует лемма, связывающая комбинацию x и y, выражающаяся в целых числах и поддерживающая последующую теорию делимости.

LaTeX

$$$(a_2 y_1 - y_0) a y + y_2 - (a_2 x_1 - x_0) = y_2 - a_2 y_1 + y_0 + a_2 (y_n1 \\cdot a y + y_1 - x_n1) - (y_n0 \\cdot a y + y_0 - x_n0).$$$

Lean4

theorem x_sub_y_dvd_pow_lem (y2 y1 y0 yn1 yn0 xn1 xn0 ay a2 : ℤ) :
    (a2 * yn1 - yn0) * ay + y2 - (a2 * xn1 - xn0) =
      y2 - a2 * y1 + y0 + a2 * (yn1 * ay + y1 - xn1) - (yn0 * ay + y0 - xn0) :=
  by ring

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