English
For any p prime and R a commutative ring, the following auxiliary relation holds: xInTermsOfW p R n · C(p^n) = X_n − ∑_{i=0}^{n-1} C(p^i) (xInTermsOfW p R i)^{p^{(n−i)}}.
Русский
Для простого p и кольца R верна вспомогательная связь: xInTermsOfW p R n · C(p^n) = X_n − ∑_{i=0}^{n-1} C(p^i) (xInTermsOfW p R i)^{p^{(n−i)}}.
LaTeX
$$$ xInTermsOfW\ p\ R\ n \; \cdot\; C((p : R)^n) = X_n - \sum_{i=0}^{n-1} C((p : R)^i) \cdot xInTermsOfW\ p\ R\ i^{p^{(n-i)}} $$$
Lean4
theorem xInTermsOfW_aux [Invertible (p : R)] (n : ℕ) :
xInTermsOfW p R n * C ((p : R) ^ n) = X n - ∑ i ∈ range n, C ((p : R) ^ i) * xInTermsOfW p R i ^ p ^ (n - i) := by
rw [xInTermsOfW_eq, mul_assoc, ← C_mul, ← mul_pow, invOf_mul_self, one_pow, C_1, mul_one]
