mul_polyOfInterest_aux2 — Mathlib

English

Another decomposition expresses wittPolyProd p n as the sum of the previous product and the remainder term, up to scalar multiples.

Русский

Другое разложение выражает wittPolyProd p n через предыдущую часть произведения и остаток, с учётом скалярных множителей.

LaTeX

$$$ wittPolyProd(p,n) = (p^n) wittMul(p,n) + wittPolyProdRemainder(p,n)$$$

Lean4

theorem mul_polyOfInterest_aux2 (n : ℕ) : (p : 𝕄) ^ n * wittMul p n + wittPolyProdRemainder p n = wittPolyProd p n :=
  by
  convert mul_polyOfInterest_aux1 p n
  rw [sum_range_succ, add_comm, Nat.sub_self, pow_zero, pow_one]
  rfl
    -- We redeclare `p` here to locally discard the unneeded `p.Prime` hypothesis.

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