WittVector.mulN_isPoly

theorem WittVector.mulN_isPoly : ∀ (p : ℕ) [hp : Fact p.Prime] (n : ℕ), WittVector.IsPoly p fun R _Rcr x => x * ↑n := by sorry

This theorem states that multiplication by `n` is a polynomial function for all prime numbers `p` and natural numbers `n`. In this context, a "polynomial function" refers to a function that can be defined by a polynomial equation. Specifically, if `x` is an element of the ring `R` (with a specified coercion from integers), the function which maps `x` to `x * n` (where the multiplication is in the ring `R`) is a polynomial function. This holds for every prime number `p` and every natural number `n`.

More concisely: For every prime number p and natural number n, the function x ↔ x * n is a polynomial function in the ring R.