xInTermsOfW_eq — Mathlib

English

For invertible p in R, xInTermsOfW p R n equals (X_n − ∑_{i=0}^{n-1} C(p^i) xInTermsOfW p R i^{p^{(n−i)}}) · C((p^{-1})^n).

Русский

Пусть p обратимо в R. Тогда xInTermsOfW p R n = (X_n − ∑_{i=0}^{n-1} C(p^i) xInTermsOfW p R i^{p^{(n−i)}}) · C(p^{-n}).

LaTeX

$$$ xInTermsOfW\ p\ R\ n = (X_n - \sum_{i=0}^{n-1} C(p^i) \cdot xInTermsOfW\ p\ R\ i^{p^{(n-i)}}) \cdot C((p^{-1})^n) $$$

Lean4

theorem xInTermsOfW_eq [Invertible (p : R)] {n : ℕ} :
    xInTermsOfW p R n = (X n - ∑ i ∈ range n, C ((p : R) ^ i) * xInTermsOfW p R i ^ p ^ (n - i)) * C ((⅟p : R) ^ n) :=
  by rw [xInTermsOfW, ← Fin.sum_univ_eq_sum_range]

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