bind₁_wittPolynomial_xInTermsOfW
theorem bind₁_wittPolynomial_xInTermsOfW :
∀ (p : ℕ) (R : Type u_1) [inst : CommRing R] [inst_1 : Invertible ↑p] (n : ℕ),
(MvPolynomial.bind₁ (wittPolynomial p R)) (xInTermsOfW p R n) = MvPolynomial.X n
The theorem `bind₁_wittPolynomial_xInTermsOfW` states that for any natural number `p`, any type `R` where `R` is a commutative ring, and for any natural number `n`, the binding of the `n`-th `xInTermsOfW` polynomial in the Witt polynomial basis with respect to `p` and `R`, is equivalent to the `n`-th degree `1` monomial (denoted as `MvPolynomial.X n`). In mathematical terms, this theorem asserts that applying the Witt polynomial transformation to the `xInTermsOfW` basis recovers the original monomial basis.
More concisely: For any commutative ring R and natural number n, the n-th Witt polynomial in the basis of xInTermsOfW with respect to a prime p is equivalent to the n-th degree monomial X^n in R.
|
wittPolynomial_zmod_self
theorem wittPolynomial_zmod_self :
∀ (p n : ℕ),
wittPolynomial p (ZMod (p ^ (n + 1))) (n + 1) =
(MvPolynomial.expand p) (wittPolynomial p (ZMod (p ^ (n + 1))) n)
This theorem states that for any natural numbers `p` and `n`, the `(n + 1)`-th Witt polynomial over the ring of integers modulo `p^(n+1)` is obtained by expanding the `n`-th Witt polynomial by a factor of `p`. Here, expansion by a factor of `p` transforms a polynomial `∑ aₙ xⁿ` into `∑ aₙ xⁿᵖ`. The Witt polynomial of order `n` is defined as `∑_{i ≤ n} p^i X_i^{p^{n-i}}` with coefficients in a commutative ring.
More concisely: The `(n + 1)`-th Witt polynomial over the ring of integers modulo `p^(n+1)` is obtained by expanding the `n`-th Witt polynomial by a factor of `p`, i.e., replacing each `x^k` term with `x^(pk)`.
|
map_wittPolynomial
theorem map_wittPolynomial :
∀ (p : ℕ) {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] (f : R →+* S) (n : ℕ),
(MvPolynomial.map f) (wittPolynomial p R n) = wittPolynomial p S n
The theorem `map_wittPolynomial` states that for any natural number `p`, and for any types `R` and `S` that form commutative rings, if we have a ring homomorphism `f` from `R` to `S`, then for any natural number `n`, the result of applying the map function to the `n`-th Witt polynomial (with coefficients in `R` and respect to `p`) is equal to the `n`-th Witt polynomial (with coefficients in `S` and respect to `p`). In simpler terms, the `n`-th Witt polynomial is preserved under the map from the ring `R` to the ring `S`.
More concisely: For any commutative rings R and S, any natural number n, and any ring homomorphism f from R to S, the image under f of the n-th Witt polynomial with coefficients in R and respect to some prime p is equal to the n-th Witt polynomial with coefficients in S and respect to the same prime p.
|